Commit 2023-06-23 06:08 87fdcaf6

View on Github →

chore: forward-port leanprover-community/mathlib#19116 (#5410)

Estimated changes

Modified Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

deleted def ContinuousLinearMap.toSpanSingleton

deleted theorem ContinuousLinearMap.toSpanSingleton_add

deleted theorem ContinuousLinearMap.toSpanSingleton_apply

deleted theorem ContinuousLinearMap.toSpanSingleton_smul'

deleted theorem ContinuousLinearMap.toSpanSingleton_smul

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added def ContinuousLinearMap.toSpanSingleton

added theorem ContinuousLinearMap.toSpanSingleton_add

added theorem ContinuousLinearMap.toSpanSingleton_apply

added theorem ContinuousLinearMap.toSpanSingleton_smul'

added theorem ContinuousLinearMap.toSpanSingleton_smul