Theorem LieModule.trace_toEnd_mul_eq_zero_of_traceForm_eq_zero

Modification history

2026-04-21 14:07
Mathlib/Algebra/Lie/TraceForm.lean
feat: a Lie module with trivial trace form is nilpotent over the derived subalgebra (#37622) …
Added LieModule.trace_toEnd_mul_eq_zero_of_traceForm_eq_zeroView on Github →