Commit 2025-03-29 01:26 8bd5208c

View on Github →

feat(Analysis/Normed): generalize lemmas to NormMulClass (#23376) Generalise some lemmas about NormedDivisionRing to any normed ring satisfying NormMulClass.

Estimated changes

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

deleted theorem AddChar.norm_apply

deleted theorem Filter.comap_mul_left_cobounded

deleted theorem Filter.comap_mul_right_cobounded

deleted theorem antilipschitzWith_mul_left

deleted theorem antilipschitzWith_mul_right

Modified Mathlib/Analysis/Normed/Ring/Lemmas.lean

added theorem AddChar.norm_apply

added def Dilation.mulLeft

added def Dilation.mulRight

added theorem Filter.comap_mul_left_cobounded

added theorem Filter.comap_mul_right_cobounded

added theorem antilipschitzWith_mul_left

added theorem antilipschitzWith_mul_right