Structures · Algebra
AddLeftCancelMonoid
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
- Shape
- One type argument
Extends2
Extended by2
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 by53
- isOfFinAddOrder_of_finite
- nsmul_eq_nsmul_iff_modEq
- AddLeftCancelMonoid.add_eq_zero
- AddLeftCancelMonoid.eq_zero_of_add_right
- addOrderOf_pos
- AddChar.norm_apply
- addOrderOf_nsmul
- Finsupp.neLocus_add_left
- AddMonoid.ExponentExists.of_finite
- infinite_not_isOfFinAddOrder
- AddLeftCancelMonoid.eq_zero_of_add_left
- DFinsupp.neLocus_add_left
- finite_multiples
- Function.mulSupport_one_add
- Function.mulSupport_one_add'
- injective_nsmul_iff_not_isOfFinAddOrder
- infinite_multiples
- multiplesEquivMultiples
- DirectSum.coe_of_mul_apply_add
- AddChar.inv_apply_eq_conj
- List.eq_of_sum_take_eq
- DirectSum.coe_decompose_mul_add_of_left_mem
- AddMonoid.exponent_ne_zero_of_finite
- AddLeftCancelMonoid.add_ne_zero
- Nat.card_addSubmonoidMultiples
- AddLeftCancelMonoid.toAddMonoid
- Positive.addLeftCancelSemigroup
- addSubmonoidOfIdempotent
- AddMonoid.neZero_exponent_of_finite
- Pi.addLeftCancelMonoid
- Colex.instAddLeftCancelMonoid
- addOrderOf_eq_card_multiples
- nsmul_inj_iff_of_addOrderOf_eq_zero
- nsmul_inj_mod
- OrderDual.instAddLeftCancelMonoid
- AddLeftCancelMonoid.toIsLeftCancelAdd
- AddMonoid.one_lt_exponent
- multiplesEquivMultiples_apply
- FunLike.addLeftCancelMonoid
- DirectSum.decompose_mul_add_left
- ULift.addLeftCancelMonoid
- AddLeftCancelMonoid.to_faithfulVAdd_addOpposite
- AddOpposite.instAddRightCancelMonoid
- AddLeftCancelMonoid.toAddLeftCancelSemigroup
- Function.Injective.addLeftCancelMonoid
- Lex.instAddLeftCancelMonoid
- Matrix.instAddLeftCancelMonoid
- mem_multiples_iff_mem_range_addOrderOf
- AddLeftCancelMonoid.addGroupOfFinite
- Multiplicative.leftCancelMonoid