Def ContinuousLinearMap.toSpanSingleton

Modification history

2024-05-17 19:31

Mathlib/Topology/Algebra/Module/Basic.lean

style: remove all isolated `where` (#12991)

Modified ContinuousLinearMap.toSpanSingleton View on Github →

2023-06-23 06:08

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

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

Modified ContinuousLinearMap.toSpanSingleton View on Github →

2023-04-12 19:26

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

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

Added ContinuousLinearMap.toSpanSingleton View on Github →