Commit 2026-11-01 22:20 16b5a1ba

View on Github →

refactor: replace padicValNat with multiplicity (#43722) This doesn't fully deprecate padicValNat, but gets most of the way there. Full deprecation will be in a follow-up PR. I directly replaced "padicValNat" with "multiplicity" in the declaration names. A few declarations of the form padicValNat.foo were manually renamed to Nat.multiplicity_foo.

Estimated changes

deleted def Imo2025Q3.fExample
modified theorem Nat.factorization_def
modified theorem Nat.fst_maxPowDvdDiv
added theorem Nat.multiplicity_self
deleted theorem Nat.padicValNat_le_self
deleted theorem Nat.padicValNat_lt_self
added theorem multiplicity_base_mul
added theorem multiplicity_base_pow
deleted theorem padicValNat_base
deleted theorem padicValNat_base_mul
deleted theorem padicValNat_base_pow
deleted theorem padicValNat_base_pow_mul
deleted theorem padicValNat_one_left
deleted theorem padicValNat_one_right
deleted theorem padicValNat_zero_left
deleted theorem padicValNat_zero_right
deleted theorem pow_padicValNat_dvd
deleted theorem padicValNat.pow_add_pow
deleted theorem padicValNat.pow_sub_pow
deleted def padicNorm
deleted def Int.padicValuation
modified theorem Padic.valuation_natCast
deleted def Rat.padicValuation
added theorem Nat.multiplicity_div'
added theorem Nat.multiplicity_div
added theorem Nat.multiplicity_mul
added theorem Nat.multiplicity_pow
deleted theorem dvd_of_one_le_padicValNat
added theorem multiplicity_choose'
added theorem multiplicity_choose
added theorem multiplicity_dvd_iff
added theorem multiplicity_factorial
added theorem multiplicity_primes
deleted theorem one_le_padicValNat_of_dvd
modified theorem padicValInt.of_nat
modified theorem padicValInt.self
deleted def padicValInt
deleted theorem padicValNat_add_le_self
deleted theorem padicValNat_choose'
deleted theorem padicValNat_choose
deleted theorem padicValNat_dvd_iff
deleted theorem padicValNat_dvd_iff_le
deleted theorem padicValNat_factorial
deleted theorem padicValNat_factorial_le
deleted theorem padicValNat_factorial_mul
deleted theorem padicValNat_le_nat_log
deleted theorem padicValNat_mul_pow_left
deleted theorem padicValNat_mul_pow_right
deleted theorem padicValNat_primes
deleted theorem padicValNat_self
modified theorem padicValRat.of_nat
deleted def padicValRat
modified theorem padicValRat_of_nat
modified theorem Nat.toNat_emultiplicity
added theorem mul_multiplicity_le
deleted theorem mul_padicValNat_le
deleted theorem padicValNat.eq_zero_iff