Theorem Padic.norm_rat_le_one_iff_padicValuation_le_one

Modification history

2025-11-27 16:30
Mathlib/NumberTheory/Padics/WithVal.lean
feat: `PadicInt` is isomorphic to the integers of the uniform space completion `(Rat.padicValuation p).Completion` (#30363) …
Added Padic.norm_rat_le_one_iff_padicValuation_le_oneView on Github →