Commit 2025-03-13 07:47 b097622c

View on Github →

chore (Analysis/Normed): rename norm_mul to norm_mul_le (#22871) Rename norm_mul of NormedRing and cousins to norm_mul_le, and norm_mul' of NormedDivisionRing to norm_mul. Split off from #22842.

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

Modified Mathlib/Analysis/CStarAlgebra/Matrix.lean

Modified Mathlib/Analysis/CStarAlgebra/lpSpace.lean

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

Modified Mathlib/Analysis/Matrix.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/Normed/Algebra/Unitization.lean

Modified Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

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

modified theorem norm_mul

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

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

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

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

Modified Mathlib/Analysis/Normed/Module/Completion.lean

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

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

modified theorem IsPowMul.restriction

modified theorem nnnorm_mul_le

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

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

Modified Mathlib/Analysis/Quaternion.lean

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Compact.lean

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean