Theorem LinearMap.span_singleton_eq_range

Modification history

2025-08-29 10:14

Mathlib/LinearAlgebra/Span/Basic.lean

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

Modified LinearMap.span_singleton_eq_range View on Github →

2023-02-14 14:29

Mathlib/LinearAlgebra/Span.lean

feat: port LinearAlgebra.Span (#2248)

Added LinearMap.span_singleton_eq_range View on Github →