Theorems · Inductive type · group theory
Monoid
Type u → Type u
A Monoid is a Semigroup with an element 1 such that 1 * a = a * 1 = a.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 3,887 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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 by5,078
Results whose statement or proof uses this declaration.
- Unitsstatement · cited by 2,804
- Units.valstatement and proof · cited by 1,966
- IsUnitstatement and proof · cited by 1,602
- one_smulstatement and proof · cited by 1,374
- MulActionstatement · cited by 1,294
- pow_zerostatement and proof · cited by 1,094
- pow_onestatement and proof · cited by 894
- Repstatement · cited by 843
- Rep.Vstatement and proof · cited by 695
- DistribMulActionstatement · cited by 584
- one_powstatement and proof · cited by 521
- map_powstatement and proof · cited by 503
Showing the 200 most cited of 5,078.