Theorem LinearEquiv.toSpanNonzeroSingleton_homothety

Modification history

2024-02-08 22:44
Mathlib/Analysis/NormedSpace/Span.lean
feat(NormedSpace): Move toSpanNonzeroSingleton to new file and add LinearIsometryEquiv (#10118)
Added LinearEquiv.toSpanNonzeroSingleton_homothetyView on Github →