Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm
Modification history
2024-02-08 22:44
Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean
feat(NormedSpace): Move toSpanNonzeroSingleton to new file and add LinearIsometryEquiv (#10118)
Modified
ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm
View on Github →
2023-04-12 19:26
Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean
feat: port Analysis.NormedSpace.ContinuousLinearMap (#3381)
Added
ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm
View on Github →