Structures · Algebra
IsRightCancelMul
A mixin for right cancellative multiplication.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds mul_right_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 by51
- mul_left_injective
- mul_right_cancel
- mulRightEmbedding
- mul_left_inj
- mul_right_cancel_iff
- mul_eq_right
- mulRightEmbedding_apply
- IsRightRegular.all
- Function.Injective.isRightCancelMul
- Finset.card_le_card_mul_right
- right_eq_mul
- CommMagma.IsRightCancelMul.toIsLeftCancelMul
- IsRightCancelMul.mul_right_cancel
- Finset.card_mul_singleton
- MonoidAlgebra.support_coeff_mul_single
- Shrink.instIsRightCancelMul
- CommMagma.IsRightCancelMul.toIsCancelMul
- TwoUniqueProds.of_covariant_right
- MonoidAlgebra.support_mul_single
- Lex.instIsRightCancelMul
- instIsRightCancelMulMonoidHom
- Set.Nontrivial.mul_right
- MulOpposite.instIsLeftCancelMul
- SkewMonoidAlgebra.support_mul_single
- mul_ne_mul_left
- Set.infinite_mul
- Pi.instIsRightCancelMul
- IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT
- Equiv.isRightCancelMul
- MulMemClass.isRightCancelMul
- right_ne_mul
- Finset.prod_eq_prod_iff_single
- Colex.instIsRightCancelMul
- OrderDual.instIsRightCancelMul
- instIsDedekindFiniteMonoidOfIsRightCancelMul
- IsRightCancelMul.mulRightStrictMono_of_mulRightMono
- mulRightEmbedding.congr_simp
- FunLike.isRightCancelMul
- instIsRightCancelMulOneHom
- MulAction.fixedBy_mul_eq_empty_iff
- Finset.card_le_card_mul_self'
- Prod.instIsRightCancelMul
- mul_right_cancel''
- instFaithfulSMulOfIsRightCancelMul
- mul_ne_right
- Finset.Nontrivial.mul_right
- Filter.Germ.instIsRightCancelMul
- Finset.inter_mul_singleton
- Set.finite_mul
- Additive.isRightCancelAdd
Ancestors0
No ancestors.