Def ContinuousLinearMap.toSpanSingletonLIE

Modification history

2026-05-21 21:58
Mathlib/Analysis/Normed/Operator/Mul.lean
refactor(Analysis): add `toSpanSingleton` isometry API (#38272) …
Added ContinuousLinearMap.toSpanSingletonLIEView on Github →