Theorem Nat.padicValNat_lt_self

Modification history

2026-09-11 16:02
Mathlib/Data/Nat/MaxPowDiv.lean
refactor(Data/Nat/MaxPowDiv): prove `padicValNat = multiplicity` earlier (#43720) …
Modified Nat.padicValNat_lt_selfView on Github →
2026-06-26 12:41
Mathlib/Data/Nat/MaxPowDiv.lean
feat(Data/Nat): a number divides a power of its own radical (#40170) …
Added Nat.padicValNat_lt_selfView on Github →