Theorem LinearIsometryEquiv.toSpanUnitSingleton_apply

Modification history

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