Theorem Valuation.norm_eq_zero

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