Def Valued.toNontriviallyNormedField:

Modification history

2025-07-04 10:05
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore: whitespace before `:` (#26727) …
Deleted Valued.toNontriviallyNormedField:View on Github →
2024-10-25 14:17
Mathlib/Topology/Algebra/Valued/NormedValued.lean
feat(Topology/Algebra/Valued/NormedValued): add lemmas for `Valued.toNormedField` (#16758) …
Added Valued.toNontriviallyNormedField:View on Github →