Theorem Nat.maxPowDvdDiv_of_pow_mul_eq

Modification history

2026-03-15 14:55
Mathlib/Data/Nat/MaxPowDiv.lean
refactor(padicValNat): redefine using `maxPowDvdDiv` (#34711) …
Added Nat.maxPowDvdDiv_of_pow_mul_eqView on Github →