Commit 2024-12-06 14:50 6581d46b

View on Github →

chore: eliminate multiplicity namespace (#19623)

Estimated changes

Modified Archive/Imo/Imo2019Q4.lean

Modified Archive/Wiedijk100Theorems/PerfectNumbers.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

added theorem Polynomial.finiteMultiplicity_X_sub_C

added theorem Polynomial.finiteMultiplicity_of_degree_pos_of_monic

deleted theorem Polynomial.multiplicity_X_sub_C_finite

deleted theorem Polynomial.multiplicity_finite_of_degree_pos_of_monic

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

Modified Mathlib/Algebra/Squarefree/Basic.lean

deleted theorem multiplicity.finite_prime_left

deleted theorem multiplicity.squarefree_iff_emultiplicity_le_one

added theorem squarefree_iff_emultiplicity_le_one

Modified Mathlib/Data/Nat/Choose/Factorization.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/Real/Irrational.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

added theorem Int.emultiplicity_pow_add_pow

added theorem Int.emultiplicity_pow_sub_pow

added theorem Nat.emultiplicity_pow_add_pow

added theorem Nat.emultiplicity_pow_sub_pow

added theorem emultiplicity_geom_sum₂_eq_one

added theorem emultiplicity_pow_prime_pow_sub_pow_prime_pow

added theorem emultiplicity_pow_prime_sub_pow_prime

added theorem emultiplicity_pow_sub_pow_of_prime

deleted theorem multiplicity.Int.pow_add_pow

deleted theorem multiplicity.Int.pow_sub_pow

deleted theorem multiplicity.Nat.pow_add_pow

deleted theorem multiplicity.Nat.pow_sub_pow

deleted theorem multiplicity.geom_sum₂_eq_one

deleted theorem multiplicity.pow_prime_pow_sub_pow_prime_pow

deleted theorem multiplicity.pow_prime_sub_pow_prime

deleted theorem multiplicity.pow_sub_pow_of_prime

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

modified theorem padicValNat.maxPowDiv_eq_multiplicity

modified theorem padicValRat.finite_int_prime_iff

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Multiplicity.lean

added theorem FiniteMultiplicity.def

added theorem FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq

added theorem FiniteMultiplicity.emultiplicity_eq_multiplicity

added theorem FiniteMultiplicity.emultiplicity_le_of_multiplicity_le

added theorem FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt

added theorem FiniteMultiplicity.emultiplicity_self

added theorem FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd

added theorem FiniteMultiplicity.le_multiplicity_of_le_emultiplicity

added theorem FiniteMultiplicity.le_multiplicity_of_pow_dvd

added theorem FiniteMultiplicity.lt_multiplicity_of_lt_emultiplicity

added theorem FiniteMultiplicity.mul_iff

added theorem FiniteMultiplicity.mul_left

added theorem FiniteMultiplicity.mul_right

added theorem FiniteMultiplicity.multiplicity_add_of_gt

added theorem FiniteMultiplicity.multiplicity_eq_iff

added theorem FiniteMultiplicity.multiplicity_le_multiplicity_iff

added theorem FiniteMultiplicity.multiplicity_lt_iff_not_dvd

added theorem FiniteMultiplicity.ne_zero

added theorem FiniteMultiplicity.neg_iff

added theorem FiniteMultiplicity.not_dvd_of_one_right

added theorem FiniteMultiplicity.not_iff_forall

added theorem FiniteMultiplicity.not_of_isUnit_left

added theorem FiniteMultiplicity.not_of_one_left

added theorem FiniteMultiplicity.not_of_unit_left

added theorem FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt

added theorem FiniteMultiplicity.not_unit

added theorem FiniteMultiplicity.one_right

added theorem FiniteMultiplicity.or_of_add

added theorem FiniteMultiplicity.pow

added theorem FiniteMultiplicity.pow_dvd_iff_le_multiplicity

added theorem Int.finiteMultiplicity_iff

added theorem Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs

deleted theorem Int.multiplicity_finite_iff

deleted theorem Int.multiplicity_finite_iff_natAbs_finite

added theorem Nat.finiteMultiplicity_iff

deleted theorem Nat.multiplicity_finite_iff

added theorem Prime.finiteMultiplicity_mul

deleted theorem Prime.multiplicity_finite_mul

modified theorem emultiplicity_lt_top

added theorem finiteMultiplicity_iff_emultiplicity_ne_top

added theorem finiteMultiplicity_mul_aux

added theorem finiteMultiplicity_of_emultiplicity_eq_natCast

deleted theorem finite_iff_emultiplicity_ne_top

deleted theorem finite_of_emultiplicity_eq_natCast

deleted theorem multiplicity.Finite.def

deleted theorem multiplicity.Finite.emultiplicity_eq_iff_multiplicity_eq

deleted theorem multiplicity.Finite.emultiplicity_eq_multiplicity

deleted theorem multiplicity.Finite.emultiplicity_le_of_multiplicity_le

deleted theorem multiplicity.Finite.emultiplicity_lt_of_multiplicity_lt

deleted theorem multiplicity.Finite.emultiplicity_self

deleted theorem multiplicity.Finite.exists_eq_pow_mul_and_not_dvd

deleted theorem multiplicity.Finite.le_multiplicity_of_le_emultiplicity

deleted theorem multiplicity.Finite.le_multiplicity_of_pow_dvd

deleted theorem multiplicity.Finite.lt_multiplicity_of_lt_emultiplicity

deleted theorem multiplicity.Finite.mul_iff

deleted theorem multiplicity.Finite.mul_left

deleted theorem multiplicity.Finite.mul_right

deleted theorem multiplicity.Finite.multiplicity_add_of_gt

deleted theorem multiplicity.Finite.multiplicity_eq_iff

deleted theorem multiplicity.Finite.multiplicity_le_multiplicity_iff

deleted theorem multiplicity.Finite.multiplicity_lt_iff_not_dvd

deleted theorem multiplicity.Finite.ne_zero

deleted theorem multiplicity.Finite.neg_iff

deleted theorem multiplicity.Finite.not_dvd_of_one_right

deleted theorem multiplicity.Finite.not_iff_forall

deleted theorem multiplicity.Finite.not_of_isUnit_left

deleted theorem multiplicity.Finite.not_of_one_left

deleted theorem multiplicity.Finite.not_of_unit_left

deleted theorem multiplicity.Finite.not_pow_dvd_of_multiplicity_lt

deleted theorem multiplicity.Finite.not_unit

deleted theorem multiplicity.Finite.one_right

deleted theorem multiplicity.Finite.or_of_add

deleted theorem multiplicity.Finite.pow

deleted theorem multiplicity.Finite.pow_dvd_iff_le_multiplicity

deleted theorem multiplicity.finite_mul_aux

modified theorem multiplicity_add_eq_min

deleted theorem multiplicity_eq_one_of_not_finite

added theorem multiplicity_eq_one_of_not_finiteMultiplicity

modified theorem multiplicity_mul

Modified Mathlib/RingTheory/PowerSeries/Order.lean

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

added theorem FiniteMultiplicity.of_not_isUnit

added theorem FiniteMultiplicity.of_prime_left

deleted theorem multiplicity.finite_of_not_isUnit