Structures · Algebra
IsCancelMulZero
A mixin for cancellative multiplication by nonzero elements.
- Defined in
- Mathlib.Algebra.GroupWithZero.Defs
- Shape
- One type argument
Extends2
Extended by3
Concrete types that are instances17
- Int
- Nat
- Polynomial
- HahnSeries
- MonoidAlgebra
- AddMonoidAlgebra
- Associates
- MvPolynomial
- Complex.UnitClosedDisc
- Complex.UnitDisc
- Subtype
- OrderDual
- Set.Elem
- MulOpposite
- PUnit
- Lex
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by189
- Prime.irreducible
- smul_eq_zero
- smul_left_injective
- smul_right_injective
- dvd_antisymm
- IsAddTorsionFree.of_isTorsionFree
- smul_eq_zero_iff_right
- irreducible_iff_prime
- IsRegular.of_ne_zero
- emultiplicity_mul
- smul_eq_zero_iff_left
- smul_right_inj
- mul_dvd_mul_iff_right
- smul_ne_zero_iff
- Associated.of_mul_left
- IsRadical.squarefree
- dvd_prime_pow
- Dvd.dvd.antisymm
- Module.IsTorsionFree.trans_faithfulSMul
- smul_ne_zero
- FiniteMultiplicity.of_prime_left
- eq_of_prime_pow_eq
- multiplicity_mul
- Associates.dvdNotUnit_iff_lt
- squarefree_mul_iff
- Function.Injective.isCancelMulZero
- UniqueFactorizationMonoid.of_exists_prime_factors
- eq_of_forall_dvd
- ContinuousMap.norm_add_eq_max
- BoundedContinuousFunction.norm_add_eq_max
- IsPrimitiveRoot.injOn_pow_mul
- Prime.left_dvd_or_dvd_right_of_dvd_mul
- emultiplicity_pow_self
- Prime.dvd_prime_iff_associated
- prime_factors_unique
- emultiplicity_pow
- DivisorChain.second_of_chain_is_irreducible
- isUnit_of_associated_mul
- Submonoid.LocalizationMap.isCancelMulZero
- Associates.isAtom_iff
- Associates.FactorSet.prod_eq_zero_iff
- map_prime_of_factor_orderIso
- mem_list_primes_of_dvd_prod
- Finset.emultiplicity_prod
- Associated.of_pow_associated_of_prime
- Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right
- prime_dvd_prime_iff_eq
- IsAbsoluteValue.abvHom'
- multiplicity_self
- Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd