Theorem ContinuousLinearMap.toLinearMap_sum

Modification history

2026-06-10 03:47
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
feat(Topology/Algebra): use `Is*Apply` for `ContinuousLinearMap` (#39637) …
Added ContinuousLinearMap.toLinearMap_sumView on Github →