Commit 2026-03-06 17:55 54703f82

View on Github →

chore(Topology/Algebra/Valued/NormedValued): replace Valued.norm by Valuation.norm (#36284) We replace the definition Valued.norm by Valuation.norm.

Estimated changes

modified theorem PadicComplex.norm_eq_norm'
modified theorem PadicComplex.norm_eq_norm
added def Valuation.norm
added theorem Valuation.norm_add_le
added theorem Valuation.norm_def
added theorem Valuation.norm_eq_zero
added theorem Valuation.norm_nonneg
deleted def Valued.norm
deleted theorem Valued.norm_add_le
deleted theorem Valued.norm_def
deleted theorem Valued.norm_eq_zero
deleted theorem Valued.norm_nonneg