Theorem LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot
Modification history
2023-11-30 11:39
Mathlib/Algebra/Lie/Killing.lean
feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739)
Deleted LieModule.span_weight_eq_top_of_ker_traceForm_eq_botView on Github →