Commit 2023-09-04 22:10 e92aa3c8

View on Github →

feat: further theory about the Killing form of Lie algebras (#6737)

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

added theorem LieIdeal.killingForm_eq

added theorem LieIdeal.le_killingCompl_top_of_isLieAbelian

added theorem LieIdeal.mem_killingCompl

added theorem LieModule.traceForm_eq_zero_of_isNilpotent

added theorem LieModule.traceForm_eq_zero_of_isTrivial

added theorem LieSubmodule.traceForm_eq_of_le_idealizer

added theorem LieSubmodule.traceForm_eq_zero_of_isTrivial

added theorem LieSubmodule.trace_eq_trace_restrict_of_le_idealizer

Modified Mathlib/Algebra/Lie/Normalizer.lean

added theorem LieIdeal.idealizer_eq_normalizer

added def LieSubmodule.idealizer

added theorem LieSubmodule.mem_idealizer

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem LinearMap.toMatrix_pow

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.isNilpotent_trace_of_isNilpotent

Modified Mathlib/RingTheory/Nilpotent.lean

added theorem LinearMap.isNilpotent_toMatrix_iff