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 any NormedDivisionRing satisfies it.
  • Generalise some of the lemmas we currently have for NormedDivisionRing or NormedField to any normed ring satisfying NormMulClass.

Estimated changes

deleted theorem enorm_mul
deleted theorem enorm_pow
deleted def nnnormHom
deleted theorem nnnorm_mul
deleted theorem nnnorm_pow
deleted theorem nnnorm_prod
deleted def normHom
deleted theorem norm_mul
deleted theorem norm_pow
deleted theorem norm_prod
added theorem NormMulClass.induced
added theorem enorm_mul
added theorem enorm_pow
added def nnnormHom
added theorem nnnorm_mul
added theorem nnnorm_pow
added theorem nnnorm_prod
added def normHom
added theorem norm_mul
added theorem norm_pow
added theorem norm_prod