Structures · Algebra
IsCancelAdd
A mixin for cancellative addition.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances21
- Filter.Germ
- Matrix
- MonoidAlgebra
- AddMonoidAlgebra
- Finsupp
- DomAddAct
- DFinsupp
- AddMonoidHom
- ZeroHom
- MvPolynomial
- AddLocalization
- Subtype
- Prod
- OrderDual
- MulOpposite
- Fin
- Lex
- AddOpposite
- Shrink
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by114
- AddMonoidAlgebra.divOf
- AddMonoidAlgebra.divOf_add_modOf
- Matrix.isLeftRegular_iff_nonsingular
- AddMonoidAlgebra.coeff_single_mul_add
- AddMonoidAlgebra.mul_of'_divOf
- Matrix.linearIndependent_col_iff
- addLeftEmbedding_eq_addRightEmbedding
- AddMonoidAlgebra.coeff_divOf
- Function.Injective.isCancelAdd
- Matrix.Nonsingular.linearIndependent_col
- Matrix.isRightRegular_iff_nonsingular
- Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_snd
- ThreeAPFree.vadd_set
- LinearMap.IsAlt.eq_of_add_add_eq_zero
- Matrix.linearIndependent_row_iff
- AddMonoidAlgebra.coeff_mul_single_add
- AddMonoidAlgebra.divOfHom
- Matrix.Nonsingular.linearIndependent_row
- add_comm_of_exponent_two
- threeAPFree_vadd_set
- AddMonoidAlgebra.divOf_zero
- AddMonoidAlgebra.of'_mul_divOf
- Set.AddAntidiagonal.eq_of_fst_eq_fst
- AddLocalization.mk_left_injective
- Set.natCard_add_le
- AddMonoidAlgebra.divOf.congr_simp
- AddMonoidAlgebra.add_divOf
- AddLocalization.mk_eq_mk_iff'
- Odd.pow_add_pow_eq_zero
- linearIndependent_iffₒₛ
- AddMonoidAlgebra.zero_divOf
- threeAPFree_insert
- AddMonoidAlgebra.of'_divOf
- Fintype.linearIndependent_iffₒₛ
- IsSemilinearSet.isProperSemilinearSet
- not_linearIndepOn_finset_iffₒₛ
- IsLinearSet.isProperSemilinearSet
- AddMonoidAlgebra.support_coeff_divOf
- AddMonoidAlgebra.divOf_add
- Set.AddAntidiagonal.finite_of_isPWO
- Matrix.Nonsingular.mul
- Set.AddAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd
- AddCommute.of_addOrderOf_dvd_two
- IsIdempotentElem.add_iff
- AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero
- AddMonoidAlgebra.modOf_add_divOf
- DFinsupp.instIsCancelAdd
- instPosSMulStrictMono
- UniqueSums.of_same
- ThreeAPFree.eq_right