Structures · Algebra
IsLeftCancelMulZero
A mixin for left cancellative multiplication by nonzero elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Shape
- One type argument · adds mul_left_cancel_of_ne_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances9
- Polynomial
- MonoidAlgebra
- AddMonoidAlgebra
- Ordinal
- Subtype
- OrderDual
- Set.Elem
- MulOpposite
- Lex
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- mul_right_inj'
- mul_left_cancel₀
- associated_of_dvd_dvd
- mul_dvd_mul_iff_left
- mul_right_injective₀
- dvd_antisymm_of_normalize_eq
- mul_eq_mul_left_iff
- normalize_eq_normalize
- dvd_dvd_iff_associated
- Function.Injective.isLeftCancelMulZero
- IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
- mul_eq_left₀
- normalize_eq_normalize_iff
- IsMulTorsionFree.pow_right_injective₀
- mul_right_eq_self₀
- Polynomial.subsingleton_isRoot_of_natDegree_eq_one
- IsIdempotentElem.iff_eq_zero_or_one
- PosMulReflectLT.toPosMulReflectLE
- PosMulMono.toPosMulStrictMono
- Finset.card_le_card_mul_left₀
- IsLeftCancelMulZero.to_isRightCancelMulZero
- eq_zero_of_mul_eq_self_right
- instLeftCancelMonoidSubtypeMemSubmonoidNonZeroDivisorsOfIsLeftCancelMulZero
- instIsDedekindFiniteMonoidOfIsLeftCancelMulZero
- Lex.instIsLeftCancelMulZero
- IsMulTorsionFree.pow_right_inj₀
- Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq
- NormalizationMonoid.ofRightInverse
- MulOpposite.instIsRightCancelMulZeroOfIsLeftCancelMulZero
- instDecidableRelAssociatedOfIsLeftCancelMulZeroOfDvd
- Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd
- IsLeftCancelMulZero.to_noZeroDivisors
- MulZeroMemClass.isLeftCancelMulZero
- Finset.card_le_card_mul_self₀
- AddMonoidAlgebra.instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums
- instNonemptyNormalizationMonoidOfIsLeftCancelMulZero
- IsLeftCancelMulZero.toFaithfulSMul_opposite
- Matrix.isAdjMatrix_iff_hadamard
- mul_right_bijective_of_finite₀
- posMulMono_iff_posMulStrictMono
- IsLeftCancelMulZero.to_isCancelMulZero
- left_eq_mul₀
- Matrix.WithConv.IsIdempotentElem.isSelfAdjoint
- Fintype.groupWithZeroOfCancel
- Metric.unitBall.instIsLeftCancelMulZero
- MonoidAlgebra.instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds
- OrderDual.instIsLeftCancelMulZero
- posMulReflectLE_iff_posMulReflectLT
Ancestors0
No ancestors.