Commit 2025-05-08 16:18 3c616a3f

View on Github →

refactor: mixin class for norm_smul with strict equality (#24003) Define a typeclass for normed modules where the norm is exactly multiplicative (not just sub-multiplicative like IsBoundedSMul, or just over fields like NormedSpace). This is a subset of #23787, leaving out the changes to NormedSpace.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

modified theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

Modified Mathlib/Analysis/Normed/Affine/AddTorsor.lean

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

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

Modified Mathlib/Analysis/Normed/MulAction.lean

added theorem NormedDivisionRing.toNormSMulClass

modified theorem norm_smul

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

Modified Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Compact.lean

modified theorem ContinuousMap.nnnorm_smul_const

modified theorem ContinuousMap.norm_smul_const

Modified Mathlib/Topology/MetricSpace/Algebra.lean

Modified Mathlib/Topology/MetricSpace/Holder.lean

added theorem HolderWith.smul_iff

Modified Mathlib/Topology/MetricSpace/HolderNorm.lean

modified theorem MemHolder.nnHolderNorm_nsmul

modified theorem MemHolder.nnHolderNorm_smul

modified theorem MemHolder.nsmul

added theorem MemHolder.smul_iff

modified theorem eHolderNorm_nsmul

modified theorem eHolderNorm_smul

Modified docs/overview.yaml

Modified docs/undergrad.yaml