Theorem Valued.toNormedField.norm_le_iff

Modification history

2026-03-06 13:45

Mathlib/Topology/Algebra/Valued/NormedValued.lean

chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …

Modified Valued.toNormedField.norm_le_iff 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.toNormedField.norm_le_iff View on Github →