Theorem Valued.toNormedField.one_le_norm_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.one_le_norm_iffView on Github →