Structures · Algebra
CommGroup
A commutative group is a group with commutative (*).
[Wikidata Q181296](https://www.wikidata.org/wiki/Q181296)
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_comm
Extends2
Extended by2
Forgetful instances
Every CommGroup is also a
Concrete types that are instances48
- SeparationQuotient
- CategoryTheory.Functor.obj
- Filter.Germ
- WithConv
- LocallyConstant
- DomMulAct
- Units
- MeasureTheory.SimpleFunc
- RestrictedProduct
- DirectLimit
- UniformFun
- UniformOnFun
- ContMDiffMap
- CategoryTheory.Limits.Cone.pt
- Tropical
- MeasureTheory.AEEqFun
- AddChar
- OneHom
- Abelianization
- PontryaginDual
- Circle
- ClassGroup
- CommRing.Pic
- ContinuousMonoidHom
- MulChar
- Pell.Solution₁
- GrpCat.carrier
- GroupLike
- Con.Quotient
- Algebra.GrothendieckGroup
- HomotopyGroup
- TopologicalAbelianization
- CommGrpCat.carrier
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- PUnit
- Lex
- AddOpposite
- HasQuotient.Quotient
- ContinuousMap
- Shrink
- Colex
- Multiplicative
- MonoidHom
How is a type an instance?
Loading the hierarchy index…
Assumed by1,181
- MulArchimedeanClass
- CommGrpCat.of
- FiniteMulArchimedeanClass
- CommGrpCat.ofHom
- CommGroup.torsion
- mul_inv_cancel_comm
- LinearOrderedCommGroup.Subgroup.genLTOne
- Rep.ofMulDistribMulAction
- MulDissociated
- mul_div_cancel_left
- MulArchimedeanClass.mk_inv
- mul_div_cancel
- Abelianization.lift
- Set.preimage_mul_const_Iio
- Subgroup.leftTransversals.diff
- div_le_div''
- Multipliable.comp_injective
- mabs_mul_le
- Set.preimage_mul_const_Iic
- CommGroup.subgroupOrderIsoSubgroupMonoidHom
- Set.preimage_mul_const_Ioi
- zpow_lt_zpow_iff_right
- MulArchimedeanClass.mk_lt_mk
- MonoidHom.transfer
- Set.inv_Iio
- MulArchimedeanClass.subgroup
- Multipliable.tendsto_cofinite_one
- Finset.mulDysonETransform
- Multipliable.subtype
- MulArchimedeanClass.mk_eq_mk
- MonoidHom.domRestrictHomKerEquiv
- IsCyclic.iff_exponent_eq_card
- div_eq_iff_eq_mul'
- Set.inv_Ioi
- CommGroup.freeRank
- Rep.FiniteCyclicGroup.resolution
- CommGroup.mem_torsion
- Rep.FiniteCyclicGroup.chainComplexFunctor
- groupCohomology.IsMulCocycle₁
- MulArchimedeanClass.orderHom
- Abelianization.commutator_subset_ker
- zpow_right_strictMono
- CommGroup.monoidHomMonoidHomEquiv
- Set.preimage_mul_const_Ici
- LinearOrderedCommGroup.Subgroup.genLTOne_unique
- MulArchimedeanClass.subsemigroup
- multipliable_nat_add_iff
- groupCohomology.IsMulCocycle₂
- Set.inv_Iic
- Set.inv_Ici
Ancestors42
- CancelCommMonoid
- CancelMonoid
- CommMagma
- CommMonoid
- CommSemigroup
- Div
- DivInvMonoid
- DivInvOneMonoid
- DivisionCommMonoid
- DivisionMonoid
- Dvd
- Group
- HDiv
- HMul
- HSMul
- Inv
- InvOneClass
- InvolutiveInv
- IsLeftCancelMul
- IsRightCancelMul
- LeftCancelMonoid
- LeftCancelSemigroup
- Monoid
- Mul
- MulAction
- MulOne
- MulOneClass
- NPow
- NSMul
- Nonempty
- OfNat
- One
- RightCancelMonoid
- RightCancelSemigroup
- SDiv
- SMul
- Semigroup
- SemigroupAction
- Torsor
- ZPow
- ZSMul
- Zero