Theorem ContinuousLinearMap.toLinearMap_one

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