Theorem ContinuousLinearMap.one_smulRight_eq_toSpanSingleton

Modification history

2025-05-07 19:19
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat(Deriv): add `derivWithin_comp_mul_left` etc (#24601)
Added ContinuousLinearMap.one_smulRight_eq_toSpanSingletonView on Github →