Commit 2024-10-21 15:51 e3e46c38

View on Github →

feat: ‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖ (#18005) and prime the existing lemmas for a norm on a multiplicative group to make space for the ring ones. From GrowthInGroups

Estimated changes

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/Convex/Uniform.lean

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

added theorem nnnorm_mul_le_of_le

added theorem nnnorm_mul₃_le

added theorem norm_mul_le_of_le

added theorem norm_mul₃_le

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem norm_mul_le_of_le'

deleted theorem norm_mul_le_of_le

added theorem norm_mul₃_le'

deleted theorem norm_mul₃_le

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

Modified Mathlib/Probability/StrongLaw.lean