Theorem ContinuousLinearMap.toSpanSingletonLIE_symm_apply

Modification history

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