Commit 2023-11-29 19:15 381a16de

View on Github →

feat: generalise results about Lie module weight spans from Abelian to nilpotent Lie algebras (#8718)

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.IsKilling.ker_restrictBilinear_eq_bot_of_isCartanSubalgebra

deleted theorem LieAlgebra.IsKilling.ker_restrictBilinear_of_isCartanSubalgebra_eq_bot

added theorem LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra

modified theorem LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot

modified theorem LieModule.traceForm_eq_sum_finrank_nsmul_mul

added theorem LieModule.traceForm_weightSpace_eq

added theorem LieModule.trace_toEndomorphism_weightSpace

Modified Mathlib/Algebra/Lie/Submodule.lean

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

added theorem LieModule.shiftedWeightSpace.coe_lie_shiftedWeightSpace_apply

added def LieModule.shiftedWeightSpace.shift

added theorem LieModule.shiftedWeightSpace.toEndomorphism_eq

added def LieModule.shiftedWeightSpace

added theorem LieModule.weight.toLinear_apply_lie