Commit 2024-10-16 04:43 7994a4b9

refactor(RingTheory/Multiplicity): split to Nat-valued multiplicity and ENat-valued emultiplicity (#16881) Also rename a bunch of stuff, and move most results outside of the multiplicity namespace. Moves (note that the definition of many of these has changed slightly):

• multiplicity -> emultiplicity
• multiplicity.finite_def -> multiplicity.Finite.def
• multiplicity.not_dvd_one_of_finite_one_right -> multiplicity.Finite.not_dvd_of_one_right
• multiplicity.Int.natCast_multiplicity -> Int.natCast_emultiplicity
• multiplicity.not_finite_iff_forall -> multiplicity.Finite.not_iff_forall
• multiplicity.not_unit_of_finite -> multiplicity.Finite.not_unit
• multiplicity.finite_of_finite_mul_right -> multiplicity.Finite.mul_left
• multiplicity.pow_dvd_of_le_multiplicity -> pow_dvd_of_le_emultiplicity
• multiplicity.pow_multiplicity_dvd -> pow_multiplicity_dvd
• multiplicity.is_greatest -> not_pow_dvd_of_emultiplicity_lt
• multiplicity.is_greatest' -> multiplicity.Finite.not_pow_dvd_of_multiplicity_lt
• multiplicity.pos_of_dvd -> emultiplicity_pos_of_dvd
• multiplicity.unique -> emultiplicity_eq_of_dvd_of_not_dvd
• multiplicity.unique' -> multiplicity_eq_of_dvd_of_not_dvd
• multiplicity.le_multiplicity_of_pow_dvd -> le_emultiplicity_of_pow_dvd
• multiplicity.pow_dvd_iff_le_multiplicity -> pow_dvd_iff_le_emultiplicity
• multiplicity.multiplicity_lt_iff_not_dvd -> emultiplicity_lt_iff_not_dvd
• multiplicity.eq_coe_iff -> emultiplicity_eq_coe
• multiplicity.eq_top_iff -> emultiplicity_eq_top
• multiplicity.isUnit_left -> multiplicity.Finite.not_of_isUnit_left
• multiplicity.one_left -> emultiplicity_one_left
• multiplicity.get_one_right -> multiplicity.Finite.one_right
• multiplicity.unit_left -> multiplicity.Finite.not_of_unit_left
• multiplicity.multiplicity_eq_zero -> emultiplicity_eq_zero
• multiplicity.multiplicity_ne_zero -> emultiplicity_ne_zero
• multiplicity.eq_top_iff_not_finite -> emultiplicity_eq_top
• multiplicity.ne_top_iff_finite -> finite_iff_emultiplicity_ne_top
• multiplicity.lt_top_iff_finite -> emultiplicity_lt_top
• multiplicity.exists_eq_pow_mul_and_not_dvd -> multiplicity.Finite.exists_eq_pow_mul_and_not_dvd
• multiplicity.multiplicity_le_multiplicity_iff -> emultiplicity_le_emultiplicity_iff
• multiplicity.multiplicity_eq_multiplicity_iff -> emultiplicity_eq_emultiplicity_iff
• multiplicity.le_multiplicity_map -> le_emultiplicity_map
• multiplicity.multiplicity_map_eq -> emultiplicity_map_eq
• multiplicity.multiplicity_le_multiplicity_of_dvd_right -> emultiplicity_le_emultiplicity_of_dvd_right
• multiplicity.eq_of_associated_right -> emultiplicity_eq_of_associated_right
• multiplicity.dvd_of_multiplicity_pos -> dvd_of_emultiplicity_pos
• multiplicity.dvd_iff_multiplicity_pos -> dvd_iff_emultiplicity_pos
• multiplicity.finite_nat_iff -> Nat.multiplicity_finite_iff
• has_dvd.dvd.multiplicity_pos -> Dvd.multiplicity_pos
• multiplicity.finite_of_finite_mul_left -> multiplicity.Finite.mul_right
• multiplicity.isUnit_right -> emultiplicity_of_isUnit_right
• multiplicity.one_right -> emultiplicity_of_one_right
• multiplicity.unit_right -> emultiplicity_of_unit_right
• multiplicity.multiplicity_le_multiplicity_of_dvd_left -> emultiplicity_le_emultiplicity_of_dvd_left
• multiplicity.eq_of_associated_left -> emultiplicity_eq_of_associated_left
• multiplicity.ne_zero_of_finite -> multiplicity.Finite.ne_zero
• multiplicity.zero -> emultiplicity_zero
• multiplicity.multiplicity_zero_eq_zero_of_ne_zero -> emultiplicity_zero_eq_zero_of_ne_zero
• multiplicity.multiplicity_mk_eq_multiplicity -> emultiplicity_mk_eq_emultiplicity
• multiplicity.min_le_multiplicity_add -> min_le_emultiplicity_add
• multiplicity.neg -> emultiplicity_neg
• multiplicity.Int.natAbs -> Int.emultiplicity_natAbs
• multiplicity.multiplicity_add_of_gt -> emultiplicity_add_of_gt
• multiplicity.multiplicity_sub_of_gt -> emultiplicity_sub_of_gt
• multiplicity.multiplicity_add_eq_min -> emultiplicity_add_eq_min
• multiplicity.finite_mul -> Prime.multiplicity_finite_mul
• multiplicity.finite_mul_iff -> multiplicity.Finite.mul_iff
• multiplicity.finite_pow -> multiplicity.Finite.pow
• multiplicity.multiplicity_self -> multiplicity_self
• multiplicity.get_multiplicity_self -> multiplicity.Finite.emultiplicity_self
• multiplicity.mul' -> multiplicity_mul
• multiplicity.mul -> emultiplicity_mul
• multiplicity.Finset.prod -> Finset.emultiplicity_prod
• multiplicity.pow' -> multiplicity.Finite.multiplicity_pow
• multiplicity.pow -> emultiplicity_pow
• multiplicity.multiplicity_pow_self -> emultiplicity_pow_self
• multiplicity.multiplicity_pow_self_of_prime -> emultiplicity_pow_self_of_prime
• multiplicity.finite_int_iff_natAbs_finite -> Int.multiplicity_finite_iff_natAbs_finite
• multiplicity.finite_int_iff -> Int.multiplicity_finite_int_iff
• multiplicity.squarefree_iff_multiplicity_le_one -> multiplicity.squarefree_iff_emultiplicity_le_one
• Nat.multiplicity_eq_card_pow_dvd -> Nat.emultiplicity_eq_card_pow_dvd
• Nat.Prime.multiplicity_one -> Nat.Prime.emultiplicity_one
• Nat.Prime.multiplicity_mul -> Nat.Prime.emultiplicity_mul
• Nat.Prime.multiplicity_pow -> Nat.Prime.emultiplicity_pow
• Nat.Prime.multiplicity_self -> Nat.Prime.emultiplicity_self
• Nat.Prime.multiplicity_pow_self -> Nat.Prime.emultiplicity_pow_self
• Nat.Prime.multiplicity_factorial -> Nat.Prime.emultiplicity_factorial
• Nat.Prime.multiplicity_factorial_mul_succ -> Nat.Prime.emultiplicity_factorial_mul_succ
• Nat.Prime.multiplicity_factorial_mul -> Nat.Prime.emultiplicity_factorial_mul
• Nat.Prime.multiplicity_choose' -> Nat.Prime.emultiplicity_choose'
• Nat.Prime.multiplicity_choose -> Nat.Prime.emultiplicity_choose
• Nat.Prime.multiplicity_le_multiplicity_choose_add -> Nat.Prime.emultiplicity_le_emultiplicity_choose_add
• Nat.Prime.multiplicity_choose_prime_pow_add_multiplicity -> Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity
• Nat.Prime.multiplicity_choose_prime_pow -> Nat.Prime.emultiplicity_choose_prime_pow
• Nat.Prime.multiplicity_two_factorial_lt -> Nat.Prime.emultiplicity_two_factorial_lt
• Polynomial.multiplicity_le_one_of_separable -> Polynomial.emultiplicity_le_one_of_separable
• KummerDedekind.multiplicity_factors_map_eq_multiplicity -> KummerDedekind.emultiplicity_factors_map_eq_emultiplicity
• padicValNat.maxPowDiv_eq_multiplicity -> padicValNat.maxPowDiv_eq_emultiplicity
• padicValNat.maxPowDiv_eq_multiplicity_get -> padicValNat.maxPowDiv_eq_multiplicity
• le_multiplicity_iff_replicate_subperm_primeFactorsList -> le_emultiplicity_iff_replicate_subperm_primeFactorsList
• multiplicity_prime_le_multiplicity_image_by_factor_orderIso -> emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso
• multiplicity_prime_eq_multiplicity_image_by_factor_orderIso -> emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso
• multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalizedFactors -> emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors
• normalizedFactorsEquivOfQuotEquiv_multiplicity_eq_multiplicity -> normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity
• multiplicity_eq_multiplicity_span -> emultiplicity_eq_emultiplicity_span
• multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity -> emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity
• multiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_multiplicity -> emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity
• PowerSeries.order_eq_multiplicity_X -> PowerSeries.order_eq_emultiplicity_X
• UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors -> UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors
• UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors -> UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors
• multiplicity.addValuation -> multiplicity_addValuation
• multiplicity.addValuation_apply -> multiplicity_addValuation_apply Deletions:
• multiplicity.finite_iff_dom
• multiplicity.decidableNat
• multiplicity.decidableInt