Theorem Valuation.IsEquiv.valuedCompletion_le_one_iff

Modification history

2025-12-19 16:47
Mathlib/Topology/Algebra/Valued/WithVal.lean
feat: `adicCompletion` for `Rat` is uniform isomorphic to `Padic` (#30576)
Added Valuation.IsEquiv.valuedCompletion_le_one_iffView on Github →