Structures · Algebra
AddCancelCommMonoid
Commutative version of AddCancelMonoid.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Forgetful instances
Concrete types that are instances16
- Nat
- NNReal
- NNRat
- Matrix
- DomAddAct
- AddLocalization
- MonomialOrder.syn
- Subtype
- Prod
- OrderDual
- ULift
- Lex
- AddOpposite
- Colex
- Additive
- Multiset
How is a type an instance?
Loading the hierarchy index…
Assumed by70
- addRothNumber_map_add_left
- AddCommGroup.ModEq.add_iff_left
- HahnSeries.addVal
- Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding
- Derivation.mk'
- Finset.sum_sdiff_eq_sum_sdiff_iff
- Finset.piAntidiag_cons
- StrictConvexOn.translate_right
- Finset.HasAntidiagonal.antidiagonal_congr'
- AddCommGroup.ModEq.add_iff_right
- StrictConcaveOn.translate_right
- AddCommGroup.ModEq.add_left_cancel
- AffineAddMonoid.dim
- Finset.card_Ico_add_right
- isAddFreimanHom_antitone
- HahnSeries.addVal_apply
- HahnSeries.order_lt_order_of_eq_add_single
- AffineAddMonoid.embedding
- StrictConvex.preimage_add_right
- MvPolynomial.IsWeightedHomogeneous.pderiv
- IsAddFreimanHom.mono
- AddMonoid.exponent_eq_max'_addOrderOf
- AddCommGroup.ModEq.add_right_cancel
- HahnSeries.coeff_order_of_eq_add_single
- eq_iff_eq_of_add_eq_add
- StrictConcaveOn.translate_left
- addRothNumber_map_add_right
- Derivation.coe_mk'
- Lex.instAddCancelCommMonoid
- card_Ico_zero_add
- IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'
- addSemiconjBy_iff_eq
- Set.AddAntidiagonal.finite_of_isWF
- ne_iff_ne_of_add_eq_add
- WithTop.linearOrderedAddCommMonoidWithTop
- Matrix.instAddCancelCommMonoid
- AddSubmonoid.LocalizationMap.instAddCancelCommMonoidLocalization
- AddSubmonoid.LocalizationMap.addCancelCommMonoid
- Prod.instAddCancelCommMonoid
- Finset.piAntidiag_insert
- AddCommGroup.ModEq.add_right_cancel'
- AddCommGroup.add_modEq_left
- Derivation.coe_mk'_linearMap
- Finset.sum_sdiff_ne_sum_sdiff_iff
- AddCancelCommMonoid.toAddLeftCancelMonoid
- OrderDual.instAddCancelCommMonoid
- AddCancelCommMonoid.toIsLeftCancelAdd
- DomAddAct.instAddCancelCommMonoidOfAddOpposite
- instPosSMulStrictMonoNatOfIsOrderedAddMonoid
- StrictConvexOn.translate_left
Ancestors27
- Add
- AddAction
- AddCancelMonoid
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddZero
- AddZeroClass
- HAdd
- HVAdd
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommMonoid
- Lean.Grind.NatModule
- NSMul
- Nonempty
- OfNat
- One
- VAdd
- Zero