Theorem ContinuousLinearMap.map_neg₂

Modification history

2026-01-08 14:22
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
fix: generalize ContinuousLinearMap.map_add₂ and friends (#33750) …
Modified ContinuousLinearMap.map_neg₂View on Github →
2023-05-20 10:55
Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean
feat: port Analysis.NormedSpace.BoundedLinearMaps (#4091) …
Added ContinuousLinearMap.map_neg₂View on Github →