Structures · Algebra
AddRightCancelMonoid
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
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances9
- Matrix
- DomAddAct
- Prod
- OrderDual
- ULift
- Lex
- AddOpposite
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- AddRightCancelMonoid.nsmul_eq_nsmul_iff_modEq
- Finsupp.neLocus_add_right
- DFinsupp.neLocus_add_right
- AddRightCancelMonoid.eq_zero_of_add_right
- DirectSum.coe_decompose_mul_add_of_right_mem
- AddRightCancelMonoid.eq_zero_of_add_left
- Function.mulSupport_add_one
- AddRightCancelMonoid.injective_nsmul_iff_not_isOfFinAddOrder
- AddRightCancelMonoid.finite_multiples
- DirectSum.coe_mul_of_apply_add
- AddRightCancelMonoid.add_eq_zero
- AddRightCancelMonoid.infinite_multiples
- AddRightCancelMonoid.infinite_not_isOfFinAddOrder
- FunLike.addRightCancelMonoid
- AddRightCancelMonoid.toAddRightCancelSemigroup
- AddRightCancelMonoid.addGroupOfFinite
- Colex.instAddRightCancelMonoid
- Multiplicative.rightCancelMonoid
- ULift.addRightCancelMonoid
- Pi.addRightCancelMonoid
- AddRightCancelMonoid.Nat.card_addSubmonoidMultiples
- AddRightCancelMonoid.add_ne_zero
- AddRightCancelMonoid.toAddMonoid
- Matrix.instAddRightCancelMonoid
- AddRightCancelMonoid.toIsRightCancelAdd
- AddOpposite.instAddLeftCancelMonoid
- OrderDual.instAddRightCancelMonoid
- Positive.addRightCancelSemigroup
- AddRightCancelMonoid.nsmul_inj_mod
- Lex.instAddRightCancelMonoid
- Prod.instAddRightCancelMonoid
- AddRightCancelMonoid.nsmul_inj_iff_of_addOrderOf_eq_zero
- DirectSum.decompose_mul_add_right
- AddMonoidHom.instAddMonoidHomClassAddHom_1
- DomAddAct.instAddRightCancelMonoidOfAddOpposite
- Function.Injective.addRightCancelMonoid
- Function.mulSupport_add_one'
- AddRightCancelMonoid.faithfulVAdd