Theorem Module.End.aeval_apply_of_hasEigenvector

Modification history

2025-10-02 09:32

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

feat(LinearAlgebra/Eigenspace/Minpoly): reduce typeclass assumptions (#29898)

Modified Module.End.aeval_apply_of_hasEigenvector View on Github →

2023-06-12 21:52

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

feat: port LinearAlgebra.Eigenspace.Minpoly (#4861)

Added Module.End.aeval_apply_of_hasEigenvector View on Github →