Def NormedField.toValued

Modification history

2024-05-15 20:27

Mathlib/Topology/Algebra/NormedValued.lean

feat(Topology/Algebra/NormedValued): add correspondence (#12432) …

Added NormedField.toValued View on Github →