Commit 2023-10-19 21:13 9eb25ab7

View on Github →

feat: miscellaneous Lie algebra lemmas (#7782)

Estimated changes

Modified Mathlib/Algebra/Lie/Basic.lean

added theorem Module.Dual.lie_apply

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieAlgebra.IsKilling.restrictBilinear_killingForm

added theorem LieIdeal.restrictBilinear_killingForm

added theorem LieModule.lie_traceForm_eq_zero

modified theorem LieModule.traceForm_apply_apply

added theorem LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center

added theorem LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieSubmodule.ucs_bot_one

Modified Mathlib/Algebra/Lie/OfAssociative.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

added theorem LieAlgebra.radical_eq_top_of_isSolvable