Theorem ContinuousLinearMap.toLinearEquiv_toSpanSingletonLIE

Modification history

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