Commit 2025-01-07 21:11 0fdf47b5

chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) After refactoring the only customer of a number of declarations on MulRingNorms to AbsoluteValue instead, this now deprecates these declarations (some of which do not adhere to the naming conventions anyway). It also adds text to the module docstring of Mathlib.Analysis.Normed.Ring.Seminorm and of MulRingNorm recommending to use AbsoluteValue instead. (Hence the documentation label. There is no label for deprecating/renaming things...) We add the equivalence MulRingNorm R ≃ AbsoluteValue R ℝ and NormedField.toAbsoluteValue to match NormedField.toMulRingNorm. Finally, it renames AbsoluteValue.Equiv to AbsoluteValue.IsEquiv (it is Prop-valued) etc. (Without deprecating the old names: they have been around for less than a week and are not used anywher by name; instead, Setoid notation is used downstream.) See here on Zulip.