Commit 2026-01-08 14:22 d90e2c3c

View on Github →

fix: generalize ContinuousLinearMap.map_add₂ and friends (#33750) These are trivial and don't need a normed space. Identified in #mathlib4 > simp? infelicity @ 💬.

Estimated changes

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

deleted theorem ContinuousLinearMap.map_add₂

deleted theorem ContinuousLinearMap.map_neg₂

deleted theorem ContinuousLinearMap.map_smul₂

deleted theorem ContinuousLinearMap.map_smulₛₗ₂

deleted theorem ContinuousLinearMap.map_sub₂

deleted theorem ContinuousLinearMap.map_zero₂

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

added theorem ContinuousLinearMap.map_add₂

added theorem ContinuousLinearMap.map_neg₂

added theorem ContinuousLinearMap.map_smul₂

added theorem ContinuousLinearMap.map_smulₛₗ₂

added theorem ContinuousLinearMap.map_sub₂

added theorem ContinuousLinearMap.map_zero₂