Structures · Algebra
AddCommMagma
A commutative additive magma is a type with an addition which commutes.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds add_comm
Extends1
Extended by1
Concrete types that are instances9
- SeparationQuotient
- Matrix
- DirectLimit
- RingCon.Quotient
- ArchimedeanClass
- AddCon.Quotient
- ModuleCon.Quotient
- Prod
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- add_comm
- AddCommute.all
- le_iff_exists_add'
- addLeftEmbedding_eq_addRightEmbedding
- AddCommMagma.add_comm
- le_map_add_map_sub
- isAddRightRegular_iff_isAddRegular
- Sym2.add
- isAddLeftRegular_iff_isAddRegular
- AddConstMapClass.map_const_add
- le_map_add_map_div
- AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd
- AddCommMagma.IsLeftCancelAdd.toIsCancelAdd
- AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd
- Set.swap_mem_antidiagonal_aux
- WithBot.le_add_self
- RingCon.instAddCommMagmaQuotient
- AddCommMagma.IsRightCancelAdd.toIsCancelAdd
- ModuleCon.instAddCommMagmaQuotient
- exists_le_add_iff_le_right
- DirectLimit.instAddCommMagmaOfAddHomClass
- Matrix.instAddCommMagma
- Pi.addCommMagma
- MulOpposite.instAddCommMagma
- Function.Surjective.addCommMagma
- AddCommMagma.toAdd
- lt_add_iff_lt_right_or_exists_lt
- forall_le_add_iff_le_right
- Function.Injective.addCommMagma
- AddCon.addCommMagma
- AddCommMagma.to_isCommutative
- exists_lt_add_iff_lt_right
- SeparationQuotient.instAddCommMagma
- Set.swap_mem_antidiagonal
- forall_lt_add_iff_lt_right
- Sym2.add_mk
- Prod.addCommMagma
- le_add_iff_lt_right_or_exists_le