Theorem Valuation.norm_def

Modification history

2026-09-24 12:38
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore(Topology/Algebra/Valued/NormedValued): generalized `Valuation.norm` to `RankLeOne` (#43656)
Modified Valuation.norm_defView on Github →
2026-09-16 15:44
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore(Topology/Algebra/Valued/NormedValued): generalize Valuation.norm to Ring (#43590)
Modified Valuation.norm_defView on Github →
2026-03-06 17:55
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore(Topology/Algebra/Valued/NormedValued): replace Valued.norm by Valuation.norm (#36284) …
Added Valuation.norm_defView on Github →