Commit 2026-09-11 16:02 ac3d0c96

View on Github →

refactor(Data/Nat/MaxPowDiv): prove padicValNat = multiplicity earlier (#43720) This PR proves padicValNat = multiplicity to ease the deprecation of padicValNat.

Estimated changes

deleted theorem Nat.divMaxPow_base_mul
deleted theorem Nat.divMaxPow_base_pow
deleted theorem Nat.divMaxPow_one_left
deleted theorem Nat.divMaxPow_self
deleted theorem Nat.fst_maxPowDvdDiv
deleted theorem Nat.maxPowDvdDiv_base_mul
deleted theorem Nat.maxPowDvdDiv_base_pow
deleted theorem Nat.maxPowDvdDiv_self
deleted theorem Nat.padicValNat_le_self
deleted theorem Nat.padicValNat_lt_self
deleted theorem Nat.snd_maxPowDvdDiv
deleted def padicValNat
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
added theorem Nat.divMaxPow_base_mul
added theorem Nat.divMaxPow_base_pow
added theorem Nat.divMaxPow_one_left
added theorem Nat.divMaxPow_self
added theorem Nat.fst_maxPowDvdDiv
added theorem Nat.maxPowDvdDiv_self
added theorem Nat.padicValNat_def
added theorem Nat.snd_maxPowDvdDiv
added def padicValNat
added theorem padicValNat_base
added theorem padicValNat_base_mul
added theorem padicValNat_base_pow
added theorem padicValNat_one_left
added theorem padicValNat_one_right
added theorem padicValNat_zero_left
added theorem padicValNat_zero_right
added theorem pow_padicValNat_dvd
deleted theorem padicValNat_def