Commit 2025-03-25 09:42 756b2f7b
View on Github →feat(Analysis/Normed): Class for strict multiplicativity of norm (#22842) This PR makes the following changes:
- Define a mixin class
NormMulClass
for norms satisfying‖a * b‖ = ‖a‖ * ‖b‖
, and show that anyNormedDivisionRing
satisfies it. - Generalise some of the lemmas we currently have for
NormedDivisionRing
orNormedField
to any normed ring satisfyingNormMulClass
.