Theorem Padic.withValUniformEquiv_cast_apply

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_cast_applyView on Github →