Theorem Valued.toNormedField.norm_le_one_iff

Modification history

2024-10-25 14:17
Mathlib/Topology/Algebra/Valued/NormedValued.lean
feat(Topology/Algebra/Valued/NormedValued): add lemmas for `Valued.toNormedField` (#16758) …
Added Valued.toNormedField.norm_le_one_iffView on Github →