Commit 2024-02-08 22:44 7bb42396

View on Github →

feat(NormedSpace): Move toSpanNonzeroSingleton to new file and add LinearIsometryEquiv (#10118)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

deleted theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm

deleted theorem ContinuousLinearEquiv.coord_self

deleted theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton

deleted theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord

deleted theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety

deleted theorem ContinuousLinearMap.toSpanSingleton_homothety

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

Created Mathlib/Analysis/NormedSpace/Span.lean

added theorem ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm

added theorem ContinuousLinearEquiv.coord_self

added theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton

added theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord

added theorem LinearEquiv.toSpanNonzeroSingleton_homothety

added theorem LinearIsometryEquiv.toSpanUnitSingleton_apply

added theorem LinearMap.toSpanSingleton_homothety

Modified Mathlib/Data/IsROrC/Basic.lean

Modified Mathlib/LinearAlgebra/Span.lean

added theorem LinearEquiv.toSpanNonzeroSingleton_apply