Theorem LinearMap.toMatrix_singleton

Modification history

2024-12-20 14:57
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat: determinant of left multiplication (#19873) …
Added LinearMap.toMatrix_singletonView on Github →