Commit 2026-03-15 14:55 c0d113d7

View on Github →

refactor(padicValNat): redefine using maxPowDvdDiv (#34711)

  • rename maxPowDiv to maxPowDvdDiv;
  • make it return a / b ^ n too;
  • optimize it to use O(log (logb b a)) steps;
  • redefine padicValNat to be maxPowDvdDiv .. |>.1

Estimated changes

added def Nat.divMaxPow
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
deleted theorem Nat.maxPowDiv.go_succ
deleted theorem Nat.maxPowDiv.le_of_dvd
deleted theorem Nat.maxPowDiv.pow_dvd
deleted theorem Nat.maxPowDiv.zero
deleted theorem Nat.maxPowDiv.zero_base
deleted def Nat.maxPowDiv
added def Nat.maxPowDvdDiv
added theorem Nat.maxPowDvdDiv_self
added theorem Nat.not_dvd_divMaxPow
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.self
deleted theorem pow_padicValNat_dvd
deleted def padicValNat