Def Valued.toNormedField

Modification history

2024-05-15 20:27
Mathlib/Topology/Algebra/NormedValued.lean
feat(Topology/Algebra/NormedValued): add correspondence (#12432) …
Added Valued.toNormedFieldView on Github →