Theorem ContinuousLinearMap.toLinearMap_mul

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_mul View on Github →