Commit 2024-03-10 21:13 bbdc3c0a

View on Github →

feat: orthogonality of Lie algebra root spaces (#10879)

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

added theorem LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne

added theorem LinearMap.trace_eq_zero_of_mapsTo_ne

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

added theorem LieAlgebra.mapsTo_toEndomorphism_weightSpace_add_of_mem_rootSpace