Commit 2026-09-16 15:44 e6252500

View on Github →

chore(Topology/Algebra/Valued/NormedValued): generalize Valuation.norm to Ring (#43590)

Estimated changes

modified def Valuation.norm
modified theorem Valuation.norm_add_le
modified theorem Valuation.norm_def
modified theorem Valuation.norm_eq_zero
modified theorem Valuation.norm_nonneg