Commit 2026-01-20 20:25 bf997ce5

View on Github →

feat(Analysis/Normed): generalize smul on cts [multi-]linear maps (#33962) Allow scalar multiplication by more general types (not just normed fields) that act reasonably on the target of the map. Mostly this just involves swapping typeclass assumptions, but the file Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean needed a more intensive refactor to separate out the results that are valid over a general base ring from those that really require a NontriviallyNormedField.

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

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

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

modified theorem ContinuousLinearMap.opNorm_smul_le

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

modified theorem IsBoundedBilinearMap.continuous

modified theorem IsBoundedBilinearMap.continuous_left

modified theorem IsBoundedBilinearMap.continuous_right

modified theorem IsBoundedBilinearMap.isBigO_comp

modified theorem IsBoundedBilinearMap.isBoundedLinearMap_left

modified theorem IsBoundedBilinearMap.isBoundedLinearMap_right

modified theorem IsBoundedBilinearMap.map_sub_left

modified theorem IsBoundedBilinearMap.map_sub_right

modified theorem IsBoundedBilinearMap.symm

modified theorem IsBoundedLinearMap.isBigO_id

modified theorem IsBoundedLinearMap.neg

modified theorem IsBoundedLinearMap.smul

modified def IsBoundedLinearMap.toContinuousLinearMap

modified structure IsBoundedLinearMap

modified theorem isBoundedBilinearMap_mul

modified theorem isBoundedBilinearMap_smul

Modified Mathlib/Analysis/Normed/Operator/Mul.lean

modified theorem ContinuousLinearMap.opNorm_lsmul

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean