Structures · Algebra
IsLeftCancelMul
A mixin for left cancellative multiplication.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_left_cancel
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances12
- Filter.Germ
- DomMulAct
- OneHom
- Subtype
- Prod
- OrderDual
- MulOpposite
- Lex
- Shrink
- Colex
- Multiplicative
- MonoidHom
How is a type an instance?
Loading the hierarchy index…
Assumed by61
- mul_left_cancel
- mul_right_injective
- mul_right_inj
- mulLeftEmbedding
- mul_eq_left
- mul_left_cancel_iff
- IsLeftRegular.all
- Function.Injective.isLeftCancelMul
- Finset.card_singleton_mul
- mulLeftEmbedding_apply
- Finset.card_le_card_mul_left
- SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinder
- left_eq_mul
- IsLeftCancelMul.mul_left_cancel
- Finset.singleton_mul_inter
- MonoidAlgebra.support_coeff_single_mul
- SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_mem
- Set.Nontrivial.mul_left
- SymbolicDynamics.FullShift.isOpen_mulOccursInAt
- CommMagma.IsLeftCancelMul.toIsRightCancelMul
- Finset.Nontrivial.mul_left
- MulOpposite.instIsRightCancelMul
- instIsLeftCancelMulMonoidHom
- FunLike.isLeftCancelMul
- SymbolicDynamics.FullShift.isClosed_mulForbidden
- OrderDual.instIsLeftCancelMul
- mul_ne_mul_right
- Set.infinite_mul
- mulLeftEmbedding.congr_simp
- Equiv.isLeftCancelMul
- mul_ne_left
- left_ne_mul
- MulAction.fixedBy_mul_op_eq_empty_iff
- instIsLeftCancelMulOneHom
- Shrink.instIsLeftCancelMul
- IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono
- TwoUniqueProds.of_covariant_left
- IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT
- SimpleGraph.mulCayley_adj_mul_iff_right
- SymbolicDynamics.FullShift.isClosed_mulOccursInAt
- MulMemClass.isLeftCancelMul
- Additive.isLeftCancelAdd
- instIsLeftCancelSMulOfIsLeftCancelMul
- Pi.instIsLeftCancelMul
- instIsDedekindFiniteMonoidOfIsLeftCancelMul
- MonoidAlgebra.support_single_mul
- Prod.instIsLeftCancelMul
- Finset.card_le_card_mul_self
- Filter.Germ.instIsLeftCancelMul
- Colex.instIsLeftCancelMul
Ancestors0
No ancestors.