Theorem ContinuousLinearMap.toSpanSingletonLIE_apply

Modification history

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