Commit 2023-06-12 21:52 5d417f27

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharZero/Lemmas.lean

Created Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

added theorem Module.End.aeval_apply_of_hasEigenvector

added theorem Module.End.eigenspace_aeval_polynomial_degree_1

added theorem Module.End.hasEigenvalue_iff_isRoot

added theorem Module.End.hasEigenvalue_of_isRoot

added theorem Module.End.isRoot_of_hasEigenvalue

added theorem Module.End.ker_aeval_ring_hom'_unit_polynomial