Def ContinuousLinearMap.llcomp

Modification history

2026-05-04 20:38
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat(Mathlib/Topology): functional-analytic prereqs for PR 37984 (#38701) …
Added ContinuousLinearMap.llcompView on Github →