Theorem NormedField.valuation_apply

Modification history

2024-10-22 04:01

Mathlib/Topology/Algebra/Valued/NormedValued.lean

chore(Topology/Algebra/Valued/NormedValued): rely on TC IsUltrametricDist instead of explicit arg (#17561) …

Modified NormedField.valuation_apply View on Github →

2024-05-15 20:27

Mathlib/Topology/Algebra/NormedValued.lean

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

Added NormedField.valuation_apply View on Github →