Structures · Algebra
IsLeftCancelAdd
A mixin for left cancellative addition.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds add_left_cancel
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances17
- Filter.Germ
- Matrix
- Finsupp
- DomAddAct
- DFinsupp
- Ordinal
- AddMonoidHom
- ZeroHom
- Subtype
- Prod
- OrderDual
- MulOpposite
- Lex
- AddOpposite
- Shrink
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by87
- add_right_inj
- add_eq_left
- add_right_injective
- addLeftEmbedding
- add_left_cancel
- add_left_cancel_iff
- left_eq_add
- addLeftEmbedding_apply
- IsAddLeftRegular.all
- Finset.card_le_card_add_left
- Function.Injective.isLeftCancelAdd
- Finset.card_singleton_add
- SymbolicDynamics.FullShift.occursInAt_eq_cylinder
- WithTop.add_left_inj
- ComplexShape.hasNoLoop_up'
- Finset.singleton_add_inter
- SymbolicDynamics.FullShift.isOpen_occursInAt
- add_ne_left
- SymbolicDynamics.FullShift.Pattern.shift_apply_add_left_of_mem
- ComplexShape.hasNoLoop_down'
- Set.finite_add
- MvPolynomial.eq_divMonomial_single
- WithBot.add_left_inj
- MvPolynomial.eq_modMonomial_single
- IsLeftCancelAdd.add_left_cancel
- AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd
- AddCommMagma.IsLeftCancelAdd.toIsCancelAdd
- le_add_iff_lt_left_or_exists_le
- Set.Nontrivial.add_left
- AddMonoidAlgebra.support_coeff_single_mul
- lt_add_iff_lt_left_or_exists_lt
- Finset.Nontrivial.add_left
- instFaithfulVAddAddOppositeOfIsLeftCancelAdd
- instIsCharPOfIsLeftCancelAddOfCharP
- WithBot.add_left_cancel
- IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT
- instIsLeftCancelVAddOfIsLeftCancelAdd
- SymbolicDynamics.FullShift.isClosed_occursInAt
- instIsLeftCancelAddZeroHom
- exists_le_add_iff_le_right
- Finset.card_le_card_add_self
- SymbolicDynamics.FullShift.Subshift.ofForbidden
- OrderDual.instIsLeftCancelAdd
- addLeftEmbedding.congr_simp
- instIsDedekindFiniteAddMonoidOfIsLeftCancelAdd
- AddMemClass.isLeftCancelAdd
- Pi.instIsLeftCancelAdd
- Finset.Nontrivial.add
- Equiv.isLeftCancelAdd
- ComplexShape.hasNoLoop_up
Ancestors0
No ancestors.