Def Valuation.norm

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