Def Valued.norm

Modification history

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