Theorem LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne

Modification history

2024-03-10 21:13
Mathlib/Algebra/DirectSum/LinearMap.lean
feat: orthogonality of Lie algebra root spaces (#10879)
Added LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_neView on Github →