Theorem Valuation.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) …
Added Valuation.norm_defView on Github →