Theorem ContinuousLinearMap.toSpanSingleton_smul'

Modification history

2024-12-19 20:34

Mathlib/Topology/Algebra/Module/Basic.lean

chore(Topology/Algebra/Module): split large file (#20036) …

Modified ContinuousLinearMap.toSpanSingleton_smul'View on Github →

2023-06-23 06:08

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

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

Modified ContinuousLinearMap.toSpanSingleton_smul'View on Github →

2023-04-12 19:26

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

feat: port Analysis.NormedSpace.ContinuousLinearMap (#3381)

Added ContinuousLinearMap.toSpanSingleton_smul'View on Github →