Theorem Nat.padicValNat_def

Modification history

2026-09-11 16:02
Mathlib/Data/Nat/PadicValNat.lean
refactor(Data/Nat/MaxPowDiv): prove `padicValNat = multiplicity` earlier (#43720) …
Added Nat.padicValNat_defView on Github →