Structures · Algebra
CommMagma
A commutative multiplicative magma is a type with a multiplication which commutes.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_comm
Extends1
Extended by2
Concrete types that are instances7
- SeparationQuotient
- WithConv
- DirectLimit
- SymAlg
- RingCon.Quotient
- Con.Quotient
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by44
- mul_comm
- Commute.all
- Matrix.transpose_mul
- dotProduct_comm
- Sym2.mul
- Matrix.trace_mul_comm
- star_mul'
- Matrix.transposeRingEquiv
- IsRightCancelMulZero.to_isLeftCancelMulZero
- le_iff_exists_mul'
- CommMagma.IsRightCancelMul.toIsLeftCancelMul
- CommMagma.mul_comm
- isRightRegular_iff_isRegular
- CommMagma.IsLeftCancelMul.toIsRightCancelMul
- Matrix.circulant_mul_comm
- isLeftRegular_iff_isRegular
- Matrix.hadamard_comm
- IsLeftCancelMulZero.to_isRightCancelMulZero
- mulLeftEmbedding_eq_mulRightEmbedding
- Prod.commMagma
- CommMagma.IsRightCancelMul.toIsCancelMul
- IsCommJordan.toIsJordan
- Matrix.transpose_vecMulVec
- CommMagma.to_isCommutative
- IsRightCancelMulZero.to_isCancelMulZero
- RingCon.instCommMagmaQuotient
- SeparationQuotient.instCommMagma
- Matrix.Fin.circulant_mul_comm
- Matrix.transposeRingEquiv_symm_apply
- Con.commMagma
- le_map_mul_map_div
- Sym2.mul_mk
- CommMagma.toMul
- Function.Injective.commMagma
- Function.Surjective.commMagma
- Matrix.transposeRingEquiv_apply
- instCommMagmaWithConvMatrix
- Matrix.conjTranspose_kronecker
- IsLeftCancelMulZero.to_isCancelMulZero
- Set.swap_mem_mulAntidiagonal_aux
- CommMagma.IsLeftCancelMul.toIsCancelMul
- Set.swap_mem_mulAntidiagonal
- Pi.commMagma
- DirectLimit.instCommMagmaOfMulHomClass