Theorem Module.End.aeval_apply_of_hasEigenvector

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) …
Modified Module.End.aeval_apply_of_hasEigenvectorView on Github →
2025-10-02 09:32
Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
feat(LinearAlgebra/Eigenspace/Minpoly): reduce typeclass assumptions (#29898)
Modified Module.End.aeval_apply_of_hasEigenvectorView on Github →
2023-06-12 21:52
Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
feat: port LinearAlgebra.Eigenspace.Minpoly (#4861)
Added Module.End.aeval_apply_of_hasEigenvectorView on Github →