Structures · Algebra
IsRightCancelAdd
A mixin for right cancellative addition.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds add_right_cancel
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances16
- Filter.Germ
- Matrix
- Finsupp
- DomAddAct
- DFinsupp
- AddMonoidHom
- ZeroHom
- Subtype
- Prod
- OrderDual
- MulOpposite
- Lex
- AddOpposite
- Shrink
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by90
- ComplexShape.up
- ComplexShape.down
- add_left_injective
- add_left_inj
- addRightEmbedding
- ComplexShape.up'
- add_right_cancel
- add_right_cancel_iff
- add_eq_right
- right_eq_add
- addRightEmbedding_apply
- ComplexShape.up_Rel
- ComplexShape.down_Rel
- CharP.natCast_injOn_Iio
- IsAddRightRegular.all
- Finset.card_le_card_add_right
- ComplexShape.down'
- Function.Injective.isRightCancelAdd
- addRightEmbedding.congr_simp
- ComplexShape.hasNoLoop_up'
- WithBot.add_right_inj
- ComplexShape.up'_mk
- WithTop.add_right_cancel
- Finset.card_add_singleton
- add_ne_right
- ComplexShape.embeddingDown'Add
- AddMonoidAlgebra.support_coeff_mul_single
- WithTop.add_right_inj
- ComplexShape.hasNoLoop_down'
- Set.finite_add
- ComplexShape.embeddingUp'Add
- AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd
- ComplexShape.down_mk
- ComplexShape.down'_mk
- CharP.natCast_eq_natCast
- IsRightCancelAdd.add_right_cancel
- IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT
- ComplexShape.embeddingUp'Add_f
- AddOpposite.instIsLeftCancelAdd
- ComplexShape.down'_Rel
- ComplexShape.up'.congr_simp
- Finset.card_le_card_add_self'
- Pi.instIsRightCancelAdd
- Equiv.isRightCancelAdd
- AddCommMagma.IsRightCancelAdd.toIsCancelAdd
- IsRightCancelAdd.addRightStrictMono_of_addRightMono
- Finset.sum_eq_sum_iff_single
- ComplexShape.instIsTruncGEEmbeddingUp'Add
- DFinsupp.instIsRightCancelAdd
- ComplexShape.instIsRelIffEmbeddingDown'Add
Ancestors0
No ancestors.