Theorem LinearMap.toMatrix_prodMap

Modification history

2024-08-03 13:28
Mathlib/LinearAlgebra/Matrix/ToLin.lean
chore: backports for leanprover/lean4#4814 (part 14) (#15406)
Modified LinearMap.toMatrix_prodMapView on Github →
2024-02-19 08:49
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat(LinearAlgebra/Charpoly): the characteristic polynomial of a direct sum (#10663) …
Added LinearMap.toMatrix_prodMapView on Github →