Theorem pow_padicValNat_dvd

Modification history

2026-11-01 22:20
Mathlib/Data/Nat/PadicValNat.lean
refactor: replace `padicValNat` with `multiplicity` (#43722) …
Deleted pow_padicValNat_dvdView on Github →
2026-09-11 16:02
Mathlib/Data/Nat/MaxPowDiv.lean
refactor(Data/Nat/MaxPowDiv): prove `padicValNat = multiplicity` earlier (#43720) …
Modified pow_padicValNat_dvdView on Github →
2026-03-15 14:55
Mathlib/Data/Nat/MaxPowDiv.lean
refactor(padicValNat): redefine using `maxPowDvdDiv` (#34711) …
Modified pow_padicValNat_dvdView on Github →
2023-03-22 07:28
Mathlib/NumberTheory/Padics/PadicVal.lean
feat: port NumberTheory.Padics.PadicVal (#3020)
Added pow_padicValNat_dvdView on Github →