Theorem ContinuousLinearMap.toSpanSingleton_smul'

Modification history

2025-08-29 10:14

Mathlib/Topology/Algebra/Module/LinearMap.lean

chore(LinearAlgebra/Span/Basic): some API for `toSpanSingleton` (#29086) …

Deleted ContinuousLinearMap.toSpanSingleton_smul'View on Github →

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 →