Theorems · Inductive type · group theory
CommMonoidWithZero
Type u_2 → Type u_2
A type M is a commutative “monoid with zero” if it is a commutative monoid with zero
element, and 0 is left and right absorbing.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 913 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 by1,068
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoidstatement · cited by 279
- Primestatement and proof · cited by 277
- MulCharstatement · cited by 186
- DirichletCharacterstatement and proof · cited by 161
- NormalizedGCDMonoidstatement · cited by 159
- UniqueFactorizationMonoid.normalizedFactorsstatement and proof · cited by 151
- GCDMonoid.gcdstatement and proof · cited by 143
- mul_div_cancel_left₀statement and proof · cited by 111
- Associates.factorsstatement and proof · cited by 97
- GCDMonoidstatement · cited by 96
- Associates.countstatement and proof · cited by 79
- GCDMonoid.lcmstatement and proof · cited by 78
Showing the 200 most cited of 1,068.