Theorem Module.Basis.lie_end_of_apply_eq_smul

Modification history

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