Mathlib Map

Theorems · Inductive type · group theory

CommMagma

Type u → Type u

A commutative multiplicative magma is a type with a multiplication which commutes.

Defined in
Mathlib.Algebra.Group.Defs
Cited by
57 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

mul_comm · cited by 2262mul_commCommute.all · cited by 119Commute.allMatrix.transpose_mul · cited by 14Matrix.transpose_muldotProduct_comm · cited by 13dotProduct_commSym2.mul · cited by 7Sym2.mulstar_mul' · cited by 5star_mul'Matrix.trace_mul_comm · cited by 5Matrix.trace_mul_commContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints · cited by 4ContinuousMap.starSubalge…Matrix.transposeRingEquiv · cited by 4Matrix.transposeRingEquivIsCommJordan · cited by 3IsCommJordanclosedBall_mul_singleton · cited by 2closedBall_mul_singletonZetaAsymptotics.termSum_of_lt · cited by 2ZetaAsymptotics.termSum_o…sphere_mul_singleton · cited by 2sphere_mul_singletonSubmonoid.LocalizationMap.injective_iff · cited by 2LocalizationMap.injective…Submonoid.LocalizationMap.isCancelMulZero · cited by 2LocalizationMap.isCancelM…CommMagmaCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by76

Results whose statement or proof uses this declaration.