Theorem LinearMap.trace_lie_mul_eq

Modification history

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