Theorem Valuation.norm_add_le

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