Theorem ContinuousLinearMap.map_neg₂

Modification history

2026-03-31 20:10

Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

chore: split `Topology.Algebra.Module.StrongTopology` (#37440)

Modified ContinuousLinearMap.map_neg₂ View on Github →

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 →