Theorem padicValNat_base_pow

Modification history

2026-09-11 16:02
Mathlib/Data/Nat/MaxPowDiv.lean
refactor(Data/Nat/MaxPowDiv): prove `padicValNat = multiplicity` earlier (#43720) …
Modified padicValNat_base_powView on Github →
2026-03-15 14:55
Mathlib/Data/Nat/MaxPowDiv.lean
refactor(padicValNat): redefine using `maxPowDvdDiv` (#34711) …
Added padicValNat_base_powView on Github →