Theorems · Inductive type · group theory
AddRightCancelMonoid
Type u → Type u
An additive monoid in which addition is right-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 AddRightCancelSemigroup is not enough.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 25 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 by35
Results whose statement or proof uses this declaration.
- AddRightCancelMonoid.nsmul_eq_nsmul_iff_modEqstatement and proof · cited by 3
- Finsupp.neLocus_add_rightstatement and proof · cited by 2
- DFinsupp.neLocus_add_rightstatement and proof · cited by 2
- AddRightCancelMonoid.eq_zero_of_add_rightstatement and proof · cited by 2
- DirectSum.coe_decompose_mul_add_of_right_memstatement and proof · cited by 2
- AddRightCancelMonoid.add_eq_zerostatement and proof · cited by 1
- AddRightCancelMonoid.casesOnstatement and proof · cited by 1
- AddRightCancelMonoid.eq_zero_of_add_leftstatement and proof · cited by 1
- AddRightCancelMonoid.extstatement and proof · cited by 1
- AddRightCancelMonoid.finite_multiplesstatement and proof · cited by 1
- AddRightCancelMonoid.infinite_multiplesstatement and proof · cited by 1
- AddRightCancelMonoid.injective_nsmul_iff_not_isOfFinAddOrderstatement and proof · cited by 1