Theorem Padic.withValUniformEquiv_norm_le_one_iff

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.withValUniformEquiv_norm_le_one_iffView on Github →