Theorem LinearMap.toMatrix_toSpanSingleton

Modification history

2026-02-11 11:08
Mathlib/LinearAlgebra/Matrix/ToLin.lean
chore: fix `Fintype` instances that are not used for data in types (#35102) …
Modified LinearMap.toMatrix_toSpanSingletonView on Github →
2025-09-29 07:22
Mathlib/LinearAlgebra/Matrix/ToLin.lean
refactor: `LinearMap.toMatrix_toSpanSingleton` (#29880) …
Modified LinearMap.toMatrix_toSpanSingletonView on Github →
2025-08-29 09:37
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat(Analysis/InnerProductSpace/PiL2): `(innerSL _ x).toMatrix` and `(toSpanSingleton _ x).toMatrix` (#28344) …
Added LinearMap.toMatrix_toSpanSingletonView on Github →