Theorems · Inductive type · group theory
AddLeftCancelMonoid
Type u → Type u
An additive monoid in which addition is left-cancellative.
Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so AddLeftCancelSemigroup is not enough.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 0 from the axioms · 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 by54
Results whose statement or proof uses this declaration.
- isOfFinAddOrder_of_finitestatement and proof · cited by 10
- nsmul_eq_nsmul_iff_modEqstatement and proof · cited by 4
- AddLeftCancelMonoid.add_eq_zerostatement and proof · cited by 4
- addOrderOf_posstatement and proof · cited by 3
- AddLeftCancelMonoid.eq_zero_of_add_rightstatement and proof · cited by 3
- AddChar.norm_applystatement and proof · cited by 2
- infinite_not_isOfFinAddOrderstatement and proof · cited by 2
- DFinsupp.neLocus_add_leftstatement and proof · cited by 2
- Finsupp.neLocus_add_leftstatement and proof · cited by 2
- AddMonoid.ExponentExists.of_finitestatement and proof · cited by 2
- AddLeftCancelMonoid.eq_zero_of_add_leftstatement and proof · cited by 2
- AddLeftCancelMonoid.extstatement and proof · cited by 2