Multiplicity

📁 Source: Mathlib/RingTheory/Multiplicity.lean

Statistics

Metric	Count
Definitions `FiniteMultiplicity`, `decidableMultiplicityFinite`, `decidableFiniteMultiplicity`, `emultiplicity`, `multiplicity`	5
Theorems `multiplicity_pos`, `def`, `emultiplicity_eq_iff_multiplicity_eq`, `emultiplicity_eq_multiplicity`, `emultiplicity_le_of_multiplicity_le`, `emultiplicity_lt_of_multiplicity_lt`, `emultiplicity_self`, `exists_eq_pow_mul_and_not_dvd`, `le_multiplicity_of_le_emultiplicity`, `le_multiplicity_of_pow_dvd`, `lt_multiplicity_of_lt_emultiplicity`, `mul_iff`, `mul_left`, `mul_right`, `multiplicity_add_of_gt`, `multiplicity_eq_iff`, `multiplicity_le_multiplicity_iff`, `multiplicity_lt_iff_not_dvd`, `multiplicity_pow`, `ne_zero`, `neg`, `neg_iff`, `not_dvd_of_one_right`, `not_iff_forall`, `not_of_isUnit_left`, `not_of_one_left`, `not_of_unit_left`, `not_pow_dvd_of_multiplicity_lt`, `not_unit`, `one_right`, `or_of_add`, `pow`, `pow_dvd_iff_le_multiplicity`, `emultiplicity_prod`, `emultiplicity_natAbs`, `finiteMultiplicity_iff`, `finiteMultiplicity_iff_finiteMultiplicity_natAbs`, `multiplicity_natAbs`, `natCast_emultiplicity`, `natCast_multiplicity`, `finiteMultiplicity_iff`, `finiteMultiplicity_mul`, `dvd_iff_emultiplicity_pos`, `dvd_iff_multiplicity_pos`, `dvd_of_emultiplicity_pos`, `dvd_of_multiplicity_pos`, `emultiplicity_add_eq_min`, `emultiplicity_add_of_gt`, `emultiplicity_eq_coe`, `emultiplicity_eq_emultiplicity_iff`, `emultiplicity_eq_iff_multiplicity_eq_of_ne_one`, `emultiplicity_eq_ofNat`, `emultiplicity_eq_of_associated_left`, `emultiplicity_eq_of_associated_right`, `emultiplicity_eq_of_dvd_of_not_dvd`, `emultiplicity_eq_top`, `emultiplicity_eq_zero`, `emultiplicity_eq_zero_iff_multiplicity_eq_zero`, `emultiplicity_le_emultiplicity_iff`, `emultiplicity_le_emultiplicity_of_dvd_left`, `emultiplicity_le_emultiplicity_of_dvd_right`, `emultiplicity_lt_iff_not_dvd`, `emultiplicity_lt_top`, `emultiplicity_map_eq`, `emultiplicity_mk_eq_emultiplicity`, `emultiplicity_mul`, `emultiplicity_ne_of_multiplicity_ne`, `emultiplicity_ne_zero`, `emultiplicity_neg`, `emultiplicity_of_isUnit_right`, `emultiplicity_of_one_right`, `emultiplicity_of_unit_right`, `emultiplicity_one_left`, `emultiplicity_pos_iff`, `emultiplicity_pos_of_dvd`, `emultiplicity_pow`, `emultiplicity_pow_self`, `emultiplicity_pow_self_of_prime`, `emultiplicity_sub_of_gt`, `emultiplicity_zero`, `emultiplicity_zero_eq_zero_of_ne_zero`, `finiteMultiplicity_iff_emultiplicity_ne_top`, `finiteMultiplicity_mul_aux`, `finiteMultiplicity_of_emultiplicity_eq_natCast`, `le_emultiplicity_map`, `le_emultiplicity_of_le_multiplicity`, `le_emultiplicity_of_pow_dvd`, `lt_emultiplicity_of_lt_multiplicity`, `min_le_emultiplicity_add`, `multiplicity_add_eq_min`, `multiplicity_eq_of_associated_left`, `multiplicity_eq_of_associated_right`, `multiplicity_eq_of_dvd_of_not_dvd`, `multiplicity_eq_of_emultiplicity_eq`, `multiplicity_eq_of_emultiplicity_eq_some`, `multiplicity_eq_one_of_not_finiteMultiplicity`, `multiplicity_eq_zero`, `multiplicity_eq_zero_of_coprime`, `multiplicity_le_emultiplicity`, `multiplicity_le_of_emultiplicity_le`, `multiplicity_lt_of_emultiplicity_lt`, `multiplicity_map_eq`, `multiplicity_mul`, `multiplicity_ne_zero`, `multiplicity_neg`, `multiplicity_of_isUnit_right`, `multiplicity_of_one_right`, `multiplicity_of_unit_right`, `multiplicity_pos_of_dvd`, `multiplicity_pow_self`, `multiplicity_pow_self_of_prime`, `multiplicity_self`, `multiplicity_sub_of_gt`, `multiplicity_zero_eq_zero_of_ne_zero`, `not_pow_dvd_of_emultiplicity_lt`, `pow_dvd_iff_le_emultiplicity`, `pow_dvd_of_le_emultiplicity`, `pow_dvd_of_le_multiplicity`, `pow_multiplicity_dvd`	119
Total	124

Dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`multiplicity_pos` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup`	`multiplicity`	—	`dvd_iff_multiplicity_pos`

FiniteMultiplicity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`def` 📖	mathematical	—	`FiniteMultiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	—
`emultiplicity_eq_iff_multiplicity_eq` 📖	mathematical	`FiniteMultiplicity`	`emultiplicity` `ENat` `ENat.instNatCast` `multiplicity`	—	`emultiplicity_eq_multiplicity`
`emultiplicity_eq_multiplicity` 📖	mathematical	`FiniteMultiplicity`	`emultiplicity` `ENat` `ENat.instNatCast` `multiplicity`	—	`multiplicity_eq_of_emultiplicity_eq_some`
`emultiplicity_le_of_multiplicity_le` 📖	mathematical	`FiniteMultiplicity` `multiplicity`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast`	—	`emultiplicity_eq_multiplicity` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`emultiplicity_lt_of_multiplicity_lt` 📖	mathematical	`FiniteMultiplicity` `multiplicity`	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast`	—	`emultiplicity_eq_multiplicity` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`emultiplicity_self` 📖	mathematical	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`emultiplicity` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`emultiplicity_eq_multiplicity` `multiplicity_self` `Nat.cast_one`
`exists_eq_pow_mul_and_not_dvd` 📖	mathematical	`FiniteMultiplicity`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toNatPow` `multiplicity` `semigroupDvd` `Monoid.toSemigroup`	—	`pow_multiplicity_dvd` `pow_succ` `mul_assoc` `multiplicity_eq_iff`
`le_multiplicity_of_le_emultiplicity` 📖	mathematical	`FiniteMultiplicity` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	`multiplicity`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `emultiplicity_eq_multiplicity`
`le_multiplicity_of_pow_dvd` 📖	mathematical	`FiniteMultiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	`multiplicity`	—	`le_multiplicity_of_le_emultiplicity` `le_emultiplicity_of_pow_dvd`
`lt_multiplicity_of_lt_emultiplicity` 📖	mathematical	`FiniteMultiplicity` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	`multiplicity`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `emultiplicity_eq_multiplicity`
`mul_iff` 📖	mathematical	`Prime`	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`mul_left` `mul_right` `Prime.finiteMultiplicity_mul`
`mul_left` 📖	—	`FiniteMultiplicity` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	`Dvd.dvd.trans` `dvd_mul_right`
`mul_right` 📖	—	`FiniteMultiplicity` `CommMonoid.toMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	`mul_left` `mul_comm`
`multiplicity_add_of_gt` 📖	mathematical	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `multiplicity`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`multiplicity_eq_of_emultiplicity_eq` `emultiplicity_add_of_gt` `LT.lt.trans_le` `WithTop.coe_strictMono` `multiplicity_le_emultiplicity` `emultiplicity_eq_multiplicity`
`multiplicity_eq_iff` 📖	mathematical	`FiniteMultiplicity`	`multiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`emultiplicity_eq_multiplicity`
`multiplicity_le_multiplicity_iff` 📖	mathematical	`FiniteMultiplicity`	`multiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`WithTop.coe_le_coe` `ENat.some_eq_coe` `emultiplicity_eq_multiplicity` `emultiplicity_le_emultiplicity_iff`
`multiplicity_lt_iff_not_dvd` 📖	mathematical	`FiniteMultiplicity`	`multiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_dvd_iff_le_multiplicity` `not_le`
`multiplicity_pow` 📖	mathematical	`Prime` `FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`multiplicity` `Monoid.toNatPow`	—	`emultiplicity_pow` `emultiplicity_eq_multiplicity` `pow`
`ne_zero` 📖	—	`FiniteMultiplicity` `MonoidWithZero.toMonoid`	—	—	—
`neg` 📖	mathematical	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`neg_iff`
`neg_iff` 📖	mathematical	—	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	—
`not_dvd_of_one_right` 📖	mathematical	`FiniteMultiplicity` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`semigroupDvd` `Monoid.toSemigroup`	—	`pow_mul_pow_eq_one`
`not_iff_forall` 📖	mathematical	—	`FiniteMultiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_zero` `one_dvd`
`not_of_isUnit_left` 📖	mathematical	`IsUnit`	`FiniteMultiplicity`	—	`not_unit`
`not_of_one_left` 📖	mathematical	—	`FiniteMultiplicity` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`not_of_unit_left` 📖	mathematical	—	`FiniteMultiplicity` `Units.val`	—	`not_of_isUnit_left` `Units.isUnit`
`not_pow_dvd_of_multiplicity_lt` 📖	mathematical	`FiniteMultiplicity` `multiplicity`	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`not_pow_dvd_of_emultiplicity_lt` `emultiplicity_eq_multiplicity` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`not_unit` 📖	mathematical	`FiniteMultiplicity`	`IsUnit`	—	`IsUnit.dvd` `IsUnit.pow`
`one_right` 📖	mathematical	`FiniteMultiplicity` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`multiplicity`	—	`multiplicity_eq_iff` `pow_zero` `zero_add` `pow_one` `not_dvd_of_one_right`
`or_of_add` 📖	—	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—	`Distrib.leftDistribClass`
`pow` 📖	mathematical	`Prime` `FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`Monoid.toNatPow`	—	`zero_add` `pow_one` `pow_zero` `isUnit_iff_dvd_one` `pow_succ'` `Prime.finiteMultiplicity_mul`
`pow_dvd_iff_le_multiplicity` 📖	mathematical	`FiniteMultiplicity`	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow` `multiplicity`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `pow_dvd_iff_le_emultiplicity` `emultiplicity_eq_multiplicity`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`emultiplicity_prod` 📖	mathematical	`Prime`	`emultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `prod` `CommMonoidWithZero.toCommMonoid` `sum` `ENat` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid` `instLinearOrderedAddCommMonoidWithTopENat`	—	`induction` `emultiplicity_of_one_right` `Prime.not_unit` `prod_insert` `sum_insert` `emultiplicity_mul`

Int

Definitions

Name	Category	Theorems
`decidableMultiplicityFinite` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`emultiplicity_natAbs` 📖	mathematical	—	`emultiplicity` `Nat.instMonoid` `instMonoid`	—	`natCast_emultiplicity` `emultiplicity_neg`
`finiteMultiplicity_iff` 📖	mathematical	—	`FiniteMultiplicity` `instMonoid`	—	`finiteMultiplicity_iff_finiteMultiplicity_natAbs` `Nat.finiteMultiplicity_iff` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd`
`finiteMultiplicity_iff_finiteMultiplicity_natAbs` 📖	mathematical	—	`FiniteMultiplicity` `instMonoid` `Nat.instMonoid`	—	—
`multiplicity_natAbs` 📖	mathematical	—	`multiplicity` `Nat.instMonoid` `instMonoid`	—	`multiplicity_eq_of_emultiplicity_eq` `emultiplicity_natAbs`
`natCast_emultiplicity` 📖	mathematical	—	`emultiplicity` `instMonoid` `Nat.instMonoid`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`natCast_multiplicity` 📖	mathematical	—	`multiplicity` `instMonoid` `Nat.instMonoid`	—	`multiplicity_eq_of_emultiplicity_eq` `natCast_emultiplicity`

Nat

Definitions

Name	Category	Theorems
`decidableFiniteMultiplicity` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteMultiplicity_iff` 📖	mathematical	—	`FiniteMultiplicity` `instMonoid`	—	`not_iff_not` `FiniteMultiplicity.not_iff_forall` `not_and_or` `not_ne_iff` `not_lt` `zero_dvd_iff` `Classical.by_contradiction` `lt_of_not_ge` `not_lt_of_ge` `one_pow` `Unique.instSubsingleton`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteMultiplicity_mul` 📖	mathematical	`Prime` `FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`finiteMultiplicity_mul_aux`

(root)

Definitions

Name	Category	Theorems
`FiniteMultiplicity` 📖	MathDef	20 math math: `Int.finiteMultiplicity_iff`, `FiniteMultiplicity.not_of_isUnit_left`, `finiteMultiplicity_iff_emultiplicity_ne_top`, `FiniteMultiplicity.not_of_one_left`, `emultiplicity_eq_top`, `FiniteMultiplicity.neg_iff`, `Polynomial.finiteMultiplicity_of_degree_pos_of_monic`, `Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs`, `FiniteMultiplicity.of_not_isUnit`, `emultiplicity_lt_top`, `FiniteMultiplicity.not_iff_forall`, `FiniteMultiplicity.def`, `FiniteMultiplicity.of_prime_left`, `padicValRat.finite_int_prime_iff`, `FiniteMultiplicity.not_of_unit_left`, `finiteMultiplicity_of_emultiplicity_eq_natCast`, `Polynomial.finiteMultiplicity_X_sub_C`, `FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite`, `FiniteMultiplicity.mul_iff`, `Nat.finiteMultiplicity_iff`
`emultiplicity` 📖	CompOp	93 math math: `emultiplicity_le_emultiplicity_of_dvd_left`, `Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity`, `emultiplicity_of_isUnit_right`, `normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity`, `emultiplicity_eq_emultiplicity_iff`, `emultiplicity_add_eq_min`, `Finset.emultiplicity_prod`, `emultiplicity_zero_eq_zero_of_ne_zero`, `lt_emultiplicity_of_lt_multiplicity`, `emultiplicity_of_one_right`, `emultiplicity_lt_iff_not_dvd`, `emultiplicity_le_emultiplicity_of_dvd_right`, `emultiplicity_pos_of_dvd`, `Nat.Prime.emultiplicity_factorial`, `emultiplicity_eq_of_associated_right`, `emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors`, `Nat.Prime.emultiplicity_le_emultiplicity_choose_add`, `emultiplicity_mk_eq_emultiplicity`, `FiniteMultiplicity.emultiplicity_self`, `FiniteMultiplicity.emultiplicity_eq_multiplicity`, `emultiplicity_pow_sub_pow_of_prime`, `le_emultiplicity_map`, `Nat.two_pow_sub_pow`, `Nat.Prime.emultiplicity_factorial_mul`, `multiplicity_addValuation_apply`, `emultiplicity_pow_prime_pow_sub_pow_prime_pow`, `Int.emultiplicity_pow_sub_pow`, `Nat.emultiplicity_pow_add_pow`, `FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq`, `le_emultiplicity_of_le_multiplicity`, `emultiplicity_le_emultiplicity_iff`, `emultiplicity_eq_of_associated_left`, `Nat.Prime.emultiplicity_choose'`, `emultiplicity_eq_zero_iff_multiplicity_eq_zero`, `emultiplicity_pow_self`, `KummerDedekind.emultiplicity_factors_map_eq_emultiplicity`, `emultiplicity_eq_zero`, `Nat.Prime.emultiplicity_choose`, `Int.two_pow_two_pow_add_two_pow_two_pow`, `emultiplicity_eq_top`, `emultiplicity_zero`, `Nat.emultiplicity_two_factorial_lt`, `le_emultiplicity_of_pow_dvd`, `Int.natCast_emultiplicity`, `FiniteMultiplicity.emultiplicity_le_of_multiplicity_le`, `Nat.Prime.emultiplicity_self`, `emultiplicity_one_left`, `Nat.Prime.emultiplicity_choose_prime_pow`, `Int.two_pow_sub_pow'`, `emultiplicity_eq_ofNat`, `pow_dvd_iff_le_emultiplicity`, `emultiplicity_geom_sum₂_eq_one`, `emultiplicity_map_eq`, `dvd_iff_emultiplicity_pos`, `emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso`, `emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso`, `squarefree_iff_emultiplicity_le_one`, `emultiplicity_of_unit_right`, `FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt`, `Int.emultiplicity_pow_add_pow`, `emultiplicity_lt_top`, `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity`, `UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors`, `Int.two_pow_sub_pow`, `Nat.Prime.emultiplicity_pow`, `Int.emultiplicity_natAbs`, `Nat.Prime.emultiplicity_factorial_le_div_pred`, `UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors`, `Nat.Prime.emultiplicity_one`, `Nat.Prime.emultiplicity_mul`, `emultiplicity_eq_coe`, `emultiplicity_pow_prime_sub_pow_prime`, `Int.two_pow_two_pow_sub_pow_two_pow`, `emultiplicity_pow`, `emultiplicity_eq_iff_multiplicity_eq_of_ne_one`, `min_le_emultiplicity_add`, `emultiplicity_pos_iff`, `emultiplicity_eq_of_dvd_of_not_dvd`, `Nat.Prime.emultiplicity_factorial_mul_succ`, `Nat.emultiplicity_pow_sub_pow`, `Nat.Prime.emultiplicity_pow_self`, `PowerSeries.order_eq_emultiplicity_X`, `le_emultiplicity_iff_replicate_subperm_primeFactorsList`, `emultiplicity_pow_self_of_prime`, `emultiplicity_eq_emultiplicity_span`, `Nat.emultiplicity_eq_card_pow_dvd`, `padicValNat.maxPowDiv_eq_emultiplicity`, `multiplicity_le_emultiplicity`, `emultiplicity_mul`, `Polynomial.emultiplicity_le_one_of_separable`, `padicValNat_eq_emultiplicity`, `emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity`, `emultiplicity_neg`
`multiplicity` 📖	CompOp	61 math math: `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `pow_multiplicity_dvd`, `FiniteMultiplicity.le_multiplicity_of_le_emultiplicity`, `Nat.multiplicity_eq_factorization`, `Int.natCast_multiplicity`, `padicValNat.maxPowDiv_eq_multiplicity`, `WittVector.map_frobeniusPoly.key₂`, `multiplicity_eq_zero`, `FiniteMultiplicity.multiplicity_pow`, `irreducible_pow_sup_of_ge`, `padicValRat.of_int_multiplicity`, `Dvd.multiplicity_pos`, `FiniteMultiplicity.emultiplicity_eq_multiplicity`, `FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd`, `multiplicity_eq_of_emultiplicity_eq`, `multiplicity_neg`, `FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq`, `multiplicity_le_of_emultiplicity_le`, `emultiplicity_eq_zero_iff_multiplicity_eq_zero`, `multiplicity_lt_of_emultiplicity_lt`, `multiplicity_of_unit_right`, `multiplicity_eq_of_associated_right`, `multiplicity_map_eq`, `Nat.Prime.emultiplicity_choose_prime_pow`, `padicValNat_def`, `WittVector.frobeniusPolyAux_eq`, `multiplicity_pow_self`, `multiplicity_pos_of_dvd`, `FiniteMultiplicity.multiplicity_lt_iff_not_dvd`, `multiplicity_eq_one_of_not_finiteMultiplicity`, `Polynomial.rootMultiplicity_eq_multiplicity`, `padicValRat.multiplicity_sub_multiplicity`, `padicValNat_def'`, `FiniteMultiplicity.multiplicity_eq_iff`, `multiplicity_mul`, `multiplicity_zero_eq_zero_of_ne_zero`, `Nat.Prime.multiplicity_factorial_pow`, `FiniteMultiplicity.pow_dvd_iff_le_multiplicity`, `dvd_iff_multiplicity_pos`, `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply`, `padicValRat.defn`, `FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity`, `multiplicity_eq_of_dvd_of_not_dvd`, `emultiplicity_eq_iff_multiplicity_eq_of_ne_one`, `emultiplicity_pos_iff`, `Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity`, `WittVector.map_frobeniusPoly.key₁`, `FiniteMultiplicity.le_multiplicity_of_pow_dvd`, `padicValInt.of_ne_one_ne_zero`, `multiplicity_add_eq_min`, `FiniteMultiplicity.multiplicity_le_multiplicity_iff`, `multiplicity_eq_of_associated_left`, `multiplicity_of_isUnit_right`, `multiplicity_self`, `multiplicity_le_emultiplicity`, `multiplicity_of_one_right`, `Nat.Prime.sub_one_mul_multiplicity_factorial`, `Int.multiplicity_natAbs`, `FiniteMultiplicity.one_right`, `multiplicity_pow_self_of_prime`, `multiplicity_eq_of_emultiplicity_eq_some`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_iff_emultiplicity_pos` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `emultiplicity` `semigroupDvd` `Monoid.toSemigroup`	—	`emultiplicity_pos_iff` `dvd_iff_multiplicity_pos`
`dvd_iff_multiplicity_pos` 📖	mathematical	—	`multiplicity` `semigroupDvd` `Monoid.toSemigroup`	—	`dvd_of_multiplicity_pos`
`dvd_of_emultiplicity_pos` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `emultiplicity`	`semigroupDvd` `Monoid.toSemigroup`	—	`pow_dvd_of_le_emultiplicity` `Order.add_one_le_of_lt` `pow_one`
`dvd_of_multiplicity_pos` 📖	mathematical	`multiplicity`	`semigroupDvd` `Monoid.toSemigroup`	—	`dvd_of_emultiplicity_pos` `lt_emultiplicity_of_lt_multiplicity`
`emultiplicity_add_eq_min` 📖	mathematical	—	`emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ENat` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat`	—	`lt_trichotomy` `add_comm` `emultiplicity_add_of_gt` `min_eq_left` `le_of_lt` `min_eq_right`
`emultiplicity_add_of_gt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`finiteMultiplicity_iff_emultiplicity_ne_top` `FiniteMultiplicity.emultiplicity_eq_multiplicity` `emultiplicity_eq_of_dvd_of_not_dvd` `dvd_add` `Distrib.leftDistribClass` `pow_dvd_of_le_emultiplicity` `LT.lt.le` `dvd_add_right` `Order.add_one_le_of_lt` `FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`
`emultiplicity_eq_coe` 📖	mathematical	—	`emultiplicity` `ENat` `ENat.instNatCast` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_dvd_of_le_emultiplicity` `not_pow_dvd_of_emultiplicity_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `emultiplicity_eq_of_dvd_of_not_dvd`
`emultiplicity_eq_emultiplicity_iff` 📖	mathematical	—	`emultiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`emultiplicity_le_emultiplicity_iff` `Eq.le` `Eq.ge` `le_antisymm`
`emultiplicity_eq_iff_multiplicity_eq_of_ne_one` 📖	mathematical	—	`emultiplicity` `ENat` `ENat.instNatCast` `multiplicity`	—	`multiplicity_eq_of_emultiplicity_eq_some`
`emultiplicity_eq_ofNat` 📖	mathematical	—	`emultiplicity` `Nat.instMonoid` `Monoid.toNatPow`	—	`emultiplicity_eq_coe`
`emultiplicity_eq_of_associated_left` 📖	mathematical	`Associated` `CommMonoid.toMonoid`	`emultiplicity`	—	`le_antisymm` `emultiplicity_le_emultiplicity_of_dvd_left` `Associated.dvd` `Associated.symm`
`emultiplicity_eq_of_associated_right` 📖	mathematical	`Associated`	`emultiplicity`	—	`le_antisymm` `emultiplicity_le_emultiplicity_of_dvd_right` `Associated.dvd` `Associated.symm`
`emultiplicity_eq_of_dvd_of_not_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	`emultiplicity` `ENat` `ENat.instNatCast`	—	`Dvd.dvd.trans` `pow_dvd_pow`
`emultiplicity_eq_top` 📖	mathematical	—	`emultiplicity` `Top.top` `ENat` `instTopENat` `FiniteMultiplicity`	—	—
`emultiplicity_eq_zero` 📖	mathematical	—	`emultiplicity` `ENat` `instZeroENat` `semigroupDvd` `Monoid.toSemigroup`	—	`ENat.coe_zero` `emultiplicity_eq_coe` `pow_zero` `zero_add` `pow_one` `emultiplicity_eq_top` `FiniteMultiplicity.not_iff_forall`
`emultiplicity_eq_zero_iff_multiplicity_eq_zero` 📖	mathematical	—	`emultiplicity` `ENat` `instZeroENat` `multiplicity`	—	`emultiplicity_eq_iff_multiplicity_eq_of_ne_one` `zero_ne_one`
`emultiplicity_le_emultiplicity_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_dvd_of_le_emultiplicity` `le_trans` `le_emultiplicity_of_pow_dvd` `Nat.find.congr_simp` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`emultiplicity_le_emultiplicity_of_dvd_left` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity`	—	`emultiplicity_le_emultiplicity_iff` `Dvd.dvd.trans` `pow_dvd_pow_of_dvd`
`emultiplicity_le_emultiplicity_of_dvd_right` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity`	—	`emultiplicity_le_emultiplicity_iff` `Dvd.dvd.trans`
`emultiplicity_lt_iff_not_dvd` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast` `semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_dvd_iff_le_emultiplicity` `not_le`
`emultiplicity_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `Top.top` `instTopENat` `FiniteMultiplicity`	—	—
`emultiplicity_map_eq` 📖	mathematical	—	`emultiplicity` `DFunLike.coe` `EquivLike.toFunLike`	—	`MulEquivClass.instMonoidHomClass`
`emultiplicity_mk_eq_emultiplicity` 📖	mathematical	—	`emultiplicity` `Associates` `CommMonoid.toMonoid` `Associates.instCommMonoid`	—	—
`emultiplicity_mul` 📖	mathematical	`Prime`	`emultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`FiniteMultiplicity.emultiplicity_eq_multiplicity` `FiniteMultiplicity.mul_left` `FiniteMultiplicity.mul_right` `multiplicity_mul` `emultiplicity_eq_top` `WithTop.add_eq_top` `FiniteMultiplicity.mul_iff`
`emultiplicity_ne_of_multiplicity_ne` 📖	—	—	—	—	`multiplicity_eq_of_emultiplicity_eq_some`
`emultiplicity_ne_zero` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup`	—	—
`emultiplicity_neg` 📖	mathematical	—	`emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`emultiplicity_eq_emultiplicity_iff`
`emultiplicity_of_isUnit_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`emultiplicity` `ENat` `instZeroENat`	—	`emultiplicity_eq_zero` `isUnit_of_dvd_unit`
`emultiplicity_of_one_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`emultiplicity` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ENat` `instZeroENat`	—	`emultiplicity_of_isUnit_right` `isUnit_one`
`emultiplicity_of_unit_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`emultiplicity` `Units.val` `ENat` `instZeroENat`	—	`emultiplicity_of_isUnit_right` `Units.isUnit`
`emultiplicity_one_left` 📖	mathematical	—	`emultiplicity` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Top.top` `ENat` `instTopENat`	—	`emultiplicity_eq_top` `FiniteMultiplicity.not_of_one_left`
`emultiplicity_pos_iff` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `emultiplicity` `multiplicity`	—	`Nat.instCanonicallyOrderedAdd`
`emultiplicity_pos_of_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup`	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instZeroENat` `emultiplicity`	—	`lt_emultiplicity_of_lt_multiplicity` `multiplicity_pos_of_dvd`
`emultiplicity_pow` 📖	mathematical	`Prime`	`emultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.instNatCast`	—	`pow_zero` `emultiplicity_of_one_right` `Prime.not_unit` `Nat.cast_zero` `MulZeroClass.zero_mul` `pow_succ` `emultiplicity_mul` `Nat.cast_add` `Nat.cast_one` `add_mul` `Distrib.rightDistribClass` `one_mul`
`emultiplicity_pow_self` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`emultiplicity` `Monoid.toNatPow` `ENat` `ENat.instNatCast`	—	`emultiplicity_eq_of_dvd_of_not_dvd` `dvd_refl` `pow_dvd_pow_iff`
`emultiplicity_pow_self_of_prime` 📖	mathematical	`Prime`	`emultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `ENat` `ENat.instNatCast`	—	`emultiplicity_pow_self` `Prime.ne_zero` `Prime.not_unit`
`emultiplicity_sub_of_gt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg` `emultiplicity_add_of_gt` `emultiplicity_neg`
`emultiplicity_zero` 📖	mathematical	—	`emultiplicity` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Top.top` `ENat` `instTopENat`	—	`emultiplicity_eq_top` `FiniteMultiplicity.ne_zero`
`emultiplicity_zero_eq_zero_of_ne_zero` 📖	mathematical	—	`emultiplicity` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `ENat` `instZeroENat`	—	`emultiplicity_eq_zero` `zero_dvd_iff`
`finiteMultiplicity_iff_emultiplicity_ne_top` 📖	mathematical	—	`FiniteMultiplicity`	—	—
`finiteMultiplicity_mul_aux` 📖	mathematical	`Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow` `MonoidWithZero.toMonoid`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	—
`finiteMultiplicity_of_emultiplicity_eq_natCast` 📖	mathematical	`emultiplicity` `ENat` `ENat.instNatCast`	`FiniteMultiplicity`	—	`emultiplicity_eq_top`
`le_emultiplicity_map` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `DFunLike.coe`	—	`emultiplicity_le_emultiplicity_iff` `map_pow` `map_dvd` `MonoidHomClass.toMulHomClass`
`le_emultiplicity_of_le_multiplicity` 📖	mathematical	`multiplicity`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	—	`LE.le.trans` `WithTop.coe_mono` `multiplicity_le_emultiplicity`
`le_emultiplicity_of_pow_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	—	`le_of_not_gt` `not_pow_dvd_of_emultiplicity_lt`
`lt_emultiplicity_of_lt_multiplicity` 📖	mathematical	`multiplicity`	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	—	`LT.lt.trans_le` `WithTop.coe_strictMono` `multiplicity_le_emultiplicity`
`min_le_emultiplicity_add` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `SemilatticeInf.toMin` `emultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `FiniteMultiplicity.or_of_add` `le_emultiplicity_of_pow_dvd` `Distrib.leftDistribClass`
`multiplicity_add_eq_min` 📖	mathematical	`FiniteMultiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`multiplicity` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`lt_trichotomy` `add_comm` `FiniteMultiplicity.multiplicity_add_of_gt` `min_eq_left` `le_of_lt` `min_eq_right`
`multiplicity_eq_of_associated_left` 📖	mathematical	`Associated` `CommMonoid.toMonoid`	`multiplicity`	—	`multiplicity_eq_of_emultiplicity_eq` `emultiplicity_eq_of_associated_left`
`multiplicity_eq_of_associated_right` 📖	mathematical	`Associated`	`multiplicity`	—	`multiplicity_eq_of_emultiplicity_eq` `emultiplicity_eq_of_associated_right`
`multiplicity_eq_of_dvd_of_not_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	`multiplicity`	—	`multiplicity_eq_of_emultiplicity_eq_some` `emultiplicity_eq_of_dvd_of_not_dvd`
`multiplicity_eq_of_emultiplicity_eq` 📖	mathematical	`emultiplicity`	`multiplicity`	—	—
`multiplicity_eq_of_emultiplicity_eq_some` 📖	mathematical	`emultiplicity` `ENat` `ENat.instNatCast`	`multiplicity`	—	—
`multiplicity_eq_one_of_not_finiteMultiplicity` 📖	mathematical	`FiniteMultiplicity`	`multiplicity`	—	`emultiplicity_eq_top`
`multiplicity_eq_zero` 📖	mathematical	—	`multiplicity` `semigroupDvd` `Monoid.toSemigroup`	—	`emultiplicity_eq_iff_multiplicity_eq_of_ne_one` `zero_ne_one` `emultiplicity_eq_zero`
`multiplicity_eq_zero_of_coprime` 📖	—	`multiplicity` `Nat.instMonoid`	—	—	`LT.lt.ne` `LT.lt.trans_le`
`multiplicity_le_emultiplicity` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `multiplicity` `emultiplicity`	—	`FiniteMultiplicity.emultiplicity_eq_multiplicity` `multiplicity_eq_one_of_not_finiteMultiplicity` `Nat.cast_one` `emultiplicity_eq_top`
`multiplicity_le_of_emultiplicity_le` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast`	`multiplicity`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `LE.le.trans` `multiplicity_le_emultiplicity`
`multiplicity_lt_of_emultiplicity_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast`	`multiplicity`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `LE.le.trans_lt` `multiplicity_le_emultiplicity`
`multiplicity_map_eq` 📖	mathematical	—	`multiplicity` `DFunLike.coe` `EquivLike.toFunLike`	—	`multiplicity_eq_of_emultiplicity_eq` `emultiplicity_map_eq`
`multiplicity_mul` 📖	mathematical	`Prime` `FiniteMultiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	`multiplicity`	—	`pow_multiplicity_dvd` `pow_add` `mul_dvd_mul` `FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt` `FiniteMultiplicity.mul_left` `FiniteMultiplicity.mul_right` `succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul` `FiniteMultiplicity.multiplicity_eq_iff`
`multiplicity_ne_zero` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup`	—	—
`multiplicity_neg` 📖	mathematical	—	`multiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`multiplicity_eq_of_emultiplicity_eq` `emultiplicity_neg`
`multiplicity_of_isUnit_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`multiplicity`	—	`multiplicity_eq_zero` `isUnit_of_dvd_unit`
`multiplicity_of_one_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`multiplicity` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`multiplicity_of_isUnit_right` `isUnit_one`
`multiplicity_of_unit_right` 📖	mathematical	`IsUnit` `CommMonoid.toMonoid`	`multiplicity` `Units.val`	—	`multiplicity_of_isUnit_right` `Units.isUnit`
`multiplicity_pos_of_dvd` 📖	mathematical	`semigroupDvd` `Monoid.toSemigroup`	`multiplicity`	—	`pow_one` `FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt` `multiplicity_eq_one_of_not_finiteMultiplicity`
`multiplicity_pow_self` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`multiplicity` `Monoid.toNatPow`	—	`multiplicity_eq_of_emultiplicity_eq_some` `emultiplicity_pow_self`
`multiplicity_pow_self_of_prime` 📖	mathematical	`Prime`	`multiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Monoid.toNatPow`	—	`multiplicity_pow_self` `Prime.ne_zero` `Prime.not_unit`
`multiplicity_self` 📖	mathematical	—	`multiplicity` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`FiniteMultiplicity.multiplicity_eq_iff` `pow_one` `sq` `mul_assoc` `IsCancelMulZero.toIsLeftCancelMulZero` `mul_one` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `FiniteMultiplicity.not_unit` `FiniteMultiplicity.ne_zero` `multiplicity_eq_one_of_not_finiteMultiplicity`
`multiplicity_sub_of_gt` 📖	mathematical	`multiplicity` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `FiniteMultiplicity`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg` `FiniteMultiplicity.multiplicity_add_of_gt` `FiniteMultiplicity.neg` `multiplicity_neg`
`multiplicity_zero_eq_zero_of_ne_zero` 📖	mathematical	—	`multiplicity` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`multiplicity_eq_zero` `zero_dvd_iff`
`not_pow_dvd_of_emultiplicity_lt` 📖	mathematical	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `emultiplicity` `ENat.instNatCast`	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Dvd.dvd.trans` `pow_dvd_pow`
`pow_dvd_iff_le_emultiplicity` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	—	`le_emultiplicity_of_pow_dvd` `pow_dvd_of_le_emultiplicity`
`pow_dvd_of_le_emultiplicity` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `ENat.instNatCast` `emultiplicity`	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_zero` `FiniteMultiplicity.not_iff_forall` `Nat.find_min` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`pow_dvd_of_le_multiplicity` 📖	mathematical	`multiplicity`	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow`	—	`pow_dvd_of_le_emultiplicity` `le_emultiplicity_of_le_multiplicity`
`pow_multiplicity_dvd` 📖	mathematical	—	`semigroupDvd` `Monoid.toSemigroup` `Monoid.toNatPow` `multiplicity`	—	`pow_dvd_of_le_multiplicity` `le_rfl`

---

← Back to Index