Commit 2026-09-24 12:38 d76c6faa

View on Github →

chore(Topology/Algebra/Valued/NormedValued): generalized Valuation.norm to RankLeOne (#43656)

Estimated changes

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