Theorems · Inductive type · group theory
CommGroupWithZero
Type u_2 → Type u_2
A type G₀ is a commutative “group with zero”
if it is a commutative monoid with zero element (distinct from 1)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of 0 must be 0.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Cited by
- 94 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 by113
Results whose statement or proof uses this declaration.
- mul_div_cancel₀statement and proof · cited by 77
- le_div_iff₀'statement and proof · cited by 32
- div_le_iff₀'statement and proof · cited by 28
- mul_div_mul_leftstatement and proof · cited by 25
- div_eq_div_iffstatement and proof · cited by 22
- div_lt_iff₀'statement and proof · cited by 20
- lt_div_iff₀'statement and proof · cited by 16
- div_le_div_iff₀statement and proof · cited by 11
- MonoidWithZeroHom.valueGroup.mkstatement and proof · cited by 11
- Set.preimage_const_mul_Ioi₀statement and proof · cited by 7
- RatFunc.liftMonoidWithZeroHomstatement and proof · cited by 6
- div_div_cancel₀statement and proof · cited by 5