Commit 2023-10-13 13:56 11add7fe

View on Github →

feat: a non-singular Killing form remains non-singular when restricted to a Cartan subalgebra (#7613) They key addition is the lemma LieAlgebra.IsKilling.ker_restrictBilinear_of_isCartanSubalgebra_eq_bot.

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.IsKilling.ker_killingForm_eq_bot

added theorem LieAlgebra.IsKilling.ker_restrictBilinear_of_isCartanSubalgebra_eq_bot

added theorem LieIdeal.coe_killingCompl_top

added theorem LieModule.eq_zero_of_mem_weightSpace_mem_posFitting

added theorem LieModule.traceForm_apply_lie_apply'

added theorem killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting

Modified Mathlib/Algebra/Lie/Submodule.lean

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

added theorem LieAlgebra.rootSpace_zero_eq

Modified Mathlib/Algebra/Module/Submodule/Bilinear.lean

added theorem LinearMap.ker_restrictBilinear_eq_of_codisjoint

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.exists_add_eq_of_codisjoint