Commit 2023-08-14 23:29 23eea437

View on Github →

feat: define the trace / killing forms on a Lie algebra (#6308)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Engel.lean

Created Mathlib/Algebra/Lie/Killing.lean

added theorem LieModule.traceForm_apply_apply

added theorem LieModule.traceForm_apply_lie_apply

added theorem LieModule.traceForm_comm

added theorem LieModule.traceForm_flip

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieModule.exists_forall_pow_toEndomorphism_eq_zero

added theorem LieModule.exists_lowerCentralSeries_eq_bot_of_isNilpotent

added theorem LieModule.isNilpotent_toEndomorphism_of_isNilpotent

added theorem LieModule.isNilpotent_toEndomorphism_of_isNilpotent₂

added theorem LieModule.iterate_toEndomorphism_mem_lowerCentralSeries₂

deleted theorem LieModule.nilpotent_endo_of_nilpotent_module

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.trace_comp_cycle'

added theorem LinearMap.trace_comp_cycle

added theorem LinearMap.trace_mul_cycle'

added theorem LinearMap.trace_mul_cycle