Multiplicity

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

Statistics

Metric	Count
Definitions	0
Theorems of_not_isUnit, of_prime_left, associated_finprod_pow_count, count_normalizedFactors_eq, count_normalizedFactors_eq', emultiplicity_eq_count_normalizedFactors, finprod_pow_count_eq_of_subsingleton_units, le_emultiplicity_iff_replicate_le_normalizedFactors, multiplicity_eq_count_normalizedFactors, max_power_factor, max_power_factor'	11
Total	11

FiniteMultiplicity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_not_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	FiniteMultiplicity MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	WfDvdMonoid.max_power_factor' pow_succ mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero left_ne_zero_of_mul
of_prime_left 📖	mathematical	Prime	FiniteMultiplicity MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	of_not_isUnit Prime.not_unit

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_finprod_pow_count 📖	mathematical	—	Associated MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero finprod CommMonoidWithZero.toCommMonoid Monoid.toPow Multiset.count normalizedFactors	—	Multiset.prod_map_eq_finprod Multiset.map_id' prod_normalizedFactors
count_normalizedFactors_eq 📖	mathematical	Irreducible MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike normalize semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero Monoid.toPow	Multiset.count normalizedFactors	—	Nat.cast_injective emultiplicity_eq_coe emultiplicity_eq_count_normalizedFactors
count_normalizedFactors_eq' 📖	mathematical	MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Irreducible MonoidWithZero.toMonoid DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.funLike normalize semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero Monoid.toPow	Multiset.count normalizedFactors	—	Multiset.count_eq_zero zero_notMem_normalizedFactors zero_pow count_normalizedFactors_eq
emultiplicity_eq_count_normalizedFactors 📖	mathematical	Irreducible MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	emultiplicity MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero ENat ENat.instNatCast Multiset.count DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike normalize normalizedFactors	—	le_antisymm Order.le_of_lt_add_one Nat.cast_one Nat.cast_add lt_iff_not_ge le_emultiplicity_iff_replicate_le_normalizedFactors Multiset.le_count_iff_replicate_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd le_refl
finprod_pow_count_eq_of_subsingleton_units 📖	mathematical	—	finprod CommMonoidWithZero.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Multiset.count normalizedFactors	—	associated_iff_eq associated_finprod_pow_count
le_emultiplicity_iff_replicate_le_normalizedFactors 📖	mathematical	Irreducible MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	ENat instLEENat ENat.instNatCast emultiplicity MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Multiset.replicate DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike normalize normalizedFactors	—	pow_dvd_iff_le_emultiplicity pow_zero Multiset.instCanonicallyOrderedAdd pow_succ' mul_assoc normalizedFactors_mul mul_eq_zero IsRightCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsRightCancelMulZero toIsCancelMulZero Multiset.replicate_succ normalizedFactors_irreducible Multiset.singleton_add Multiset.cons_le_cons_iff Dvd.intro Multiset.le_iff_exists_add Associated.dvd_iff_dvd_right prod_normalizedFactors Multiset.prod_add Multiset.prod_replicate Dvd.dvd.trans Associated.dvd Associated.pow_pow associated_normalize
multiplicity_eq_count_normalizedFactors 📖	mathematical	Irreducible MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	multiplicity MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Multiset.count DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike normalize normalizedFactors	—	emultiplicity_eq_count_normalizedFactors FiniteMultiplicity.emultiplicity_eq_multiplicity finiteMultiplicity_of_emultiplicity_eq_natCast

WfDvdMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
max_power_factor 📖	mathematical	Irreducible MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toPow MonoidWithZero.toMonoid	—	max_power_factor' Irreducible.not_isUnit
max_power_factor' 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	semigroupDvd SemigroupWithZero.toSemigroup MonoidWithZero.toSemigroupWithZero CommMonoidWithZero.toMonoidWithZero MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Monoid.toPow MonoidWithZero.toMonoid	—	WellFounded.has_min wellFounded_dvdNotUnit pow_zero one_mul pow_succ mul_assoc right_ne_zero_of_mul mul_comm

---

← Back to Index