Theorem Valued.norm_def

Modification history

2026-03-06 17:55

Mathlib/Topology/Algebra/Valued/NormedValued.lean

chore(Topology/Algebra/Valued/NormedValued): replace Valued.norm by Valuation.norm (#36284) …

Deleted Valued.norm_def View on Github →

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.norm_def View on Github →

2025-03-25 09:33

Mathlib/Topology/Algebra/Valued/NormedValued.lean

feat(Valued/NormedValued): add lemma on positivity of the norm (#23277) …

Added Valued.norm_def View on Github →