Structures · Algebra

Group

A Group is a Monoid with an operation ⁻¹ satisfying a⁻¹ * a = 1. There is also a division operation / such that a / b = a * b⁻¹, with a default so that a / b = a * b⁻¹ holds by definition. Use Group.ofLeftAxioms or Group.ofRightAxioms to define a group structure on a type with the minimum proof obligations. [Wikidata Q83478](https://www.wikidata.org/wiki/Q83478)

Defined in: Mathlib.Algebra.Group.Defs
Shape: One type argument · adds inv_mul_cancel

Open in Mathlib docs

Extends1

DivInvMonoid

Extended by4

Forgetful instances

Every Group is also a

Provided automatically by

CategoryTheory.GrpObj

Concrete types that are instances78

Quiver.Hom
TopCat.carrier
SeparationQuotient
CategoryTheory.Functor.obj
Filter.Germ
WithConv
LocallyConstant
DomMulAct
Units
MeasureTheory.SimpleFunc
RestrictedProduct
DirectLimit
UniformFun
UniformOnFun
ContMDiffMap
CategoryTheory.Limits.Cone.pt
CategoryTheory.End
Tropical
Matrix.SpecialLinearGroup
MeasureTheory.AEEqFun
AlgEquiv
FreeGroup
LinearEquiv
Equiv.Perm
OneHom
Polynomial.Gal
MonCat.carrier
CategoryTheory.Aut
ConjAct
DihedralGroup
QuaternionGroup
GrpCat.carrier
LinearIsometryEquiv
Field.absoluteGaloisGroup
RegularWreathProduct
ContinuousLinearEquiv
GroupLike
AffineEquiv
AffineIsometryEquiv
SpecialLinearGroup
Con.Quotient
StarAlgEquiv
IteratedWreathProduct
RelIso
HomotopyGroup
AddConstEquiv
Homeomorph
RingAut
IsometryEquiv
DilationEquiv
SemidirectProduct
MulAut
Monoid.CoprodI
CategoryTheory.PresheafOfGroups.OneCochain
RootPairing.Equiv
WeierstrassCurve.VariableChange
Matrix.ProjGenLinGroup
PresentedGroup
HNNExtension
Monoid.PushoutI
Monoid.Coprod
Rack.EnvelGroup
CoxeterMatrix.Group
CategoryTheory.PresheafOfGroups.ZeroCochain
CategoryTheory.PreGaloisCategory.AutGalois
Subtype
Prod
OrderDual
Set.Elem
ULift
MulOpposite
Lex
AddOpposite
HasQuotient.Quotient
ContinuousMap
Shrink
Colex
Multiplicative

How is a type an instance?

Loading the hierarchy index…