theorem
Module.End.ker_aeval_ring_hom'_unit_polynomial
{R : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(f : End R M)
(c : (Polynomial R)ˣ)
:
theorem
Module.End.aeval_apply_of_hasEigenvector
{R : Type v}
{M : Type w}
[CommRing R]
[AddCommGroup M]
[Module R M]
{f : End R M}
{p : Polynomial R}
{μ : R}
{x : M}
(h : f.HasEigenvector μ x)
:
theorem
Module.End.isRoot_of_hasEigenvalue
{R : Type v}
{M : Type w}
[CommRing R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
{f : End R M}
{μ : R}
(h : f.HasEigenvalue μ)
:
theorem
Module.End.hasEigenvalue_of_isRoot
{R : Type v}
{M : Type w}
[CommRing R]
[AddCommGroup M]
[Module R M]
{f : End R M}
{μ : R}
[IsDomain R]
[Module.Finite R M]
(h : (minpoly R f).IsRoot μ)
:
f.HasEigenvalue μ
theorem
Module.End.hasEigenvalue_iff_isRoot
{R : Type v}
{M : Type w}
[CommRing R]
[AddCommGroup M]
[Module R M]
{f : End R M}
{μ : R}
[IsDomain R]
[Module.Finite R M]
[NoZeroSMulDivisors R M]
:
theorem
Module.End.finite_hasEigenvalue
{R : Type v}
{M : Type w}
[CommRing R]
[AddCommGroup M]
[Module R M]
(f : End R M)
[IsDomain R]
[Module.Finite R M]
[NoZeroSMulDivisors R M]
:
noncomputable instance
Module.End.instFintypeEigenvalues
{R : Type v}
{M : Type w}
[CommRing R]
[AddCommGroup M]
[Module R M]
(f : End R M)
[IsDomain R]
[Module.Finite R M]
[NoZeroSMulDivisors R M]
:
An endomorphism of a finite-dimensional vector space has finitely many eigenvalues.
Equations
theorem
Module.End.eigenspace_aeval_polynomial_degree_1
{K : Type v}
{V : Type w}
[Field K]
[AddCommGroup V]
[Module K V]
(f : End K V)
(q : Polynomial K)
(hq : q.degree = 1)
:
theorem
Module.End.finite_spectrum
{K : Type v}
{V : Type w}
[Field K]
[AddCommGroup V]
[Module K V]
[FiniteDimensional K V]
(f : End K V)
:
An endomorphism of a finite-dimensional vector space has a finite spectrum.
theorem
Matrix.finite_spectrum
{n : Type u_1}
{R : Type u_2}
[Field R]
[Fintype n]
[DecidableEq n]
(A : Matrix n n R)
:
An n x n matrix over a field has a finite spectrum.
instance
Matrix.instFiniteSpectrum
{n : Type u_1}
{R : Type u_2}
[Field R]
[Fintype n]
[DecidableEq n]
(A : Matrix n n R)
: