Theorem LinearMap.toMatrix_smulRight

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_smulRightView on Github →
2025-09-26 06:47
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat(LinearAlgebra): trace of `LinearMap.smulRight` (#29890) …
Added LinearMap.toMatrix_smulRightView on Github →