Structures · Algebra
IsRightCancelMulZero
A mixin for right cancellative multiplication by nonzero elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Shape
- One type argument · adds mul_right_cancel_of_ne_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances8
- Polynomial
- MonoidAlgebra
- AddMonoidAlgebra
- Subtype
- OrderDual
- Set.Elem
- MulOpposite
- Lex
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- mul_left_inj'
- mul_left_injective₀
- mul_right_cancel₀
- mul_eq_mul_right_iff
- mul_eq_right₀
- eq_zero_of_mul_eq_self_left
- Function.Injective.isRightCancelMulZero
- eq_zero_or_one_of_sq_eq_self
- right_eq_mul₀
- mul_left_eq_self₀
- IsRightCancelMulZero.to_isLeftCancelMulZero
- MulPosMono.toMulPosStrictMono
- MulPosReflectLT.toMulPosReflectLE
- IsRightCancelMulZero.mul_right_cancel_of_ne_zero
- instIsDedekindFiniteMonoidOfIsRightCancelMulZero
- MulZeroMemClass.isRightCancelMulZero
- instRightCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsRightCancelMulZero
- IsRightCancelMulZero.to_isCancelMulZero
- OrderDual.instIsRightCancelMulZero
- mulPosMono_iff_mulPosStrictMono
- Finset.card_le_card_mul_right₀
- mulPosReflectLE_iff_mulPosReflectLT
- mul_left_bijective_of_finite₀
- IsRightCancelMulZero.to_noZeroDivisors
- Lex.instIsRightCancelMulZero
- MonoidAlgebra.instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds
- IsRightCancelMulZero.faithfulSMul
- Metric.unitBall.instIsRightCancelMulZero
- Polynomial.instIsRightCancelMulZeroOfIsCancelAdd
- AddMonoidAlgebra.instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums
- MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero
Ancestors0
No ancestors.