Theorem Module.End.aeval_apply_of_mem_apply_eq_smul

Modification history

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