Commit 2025-10-02 09:32 fc44d8a2

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

modified theorem Module.End.aeval_apply_of_hasEigenvector

modified theorem Module.End.hasEigenvalue_iff_isRoot

modified theorem Module.End.hasEigenvalue_of_isRoot

modified theorem Module.End.isRoot_of_hasEigenvalue

modified theorem Module.End.ker_aeval_ring_hom'_unit_polynomial