Theorems · Theorem · linear algebra

Module.End.hasEigenvalue_iff_isRoot_charpoly

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Free R M] [inst_5 : Module.Finite R M] (f : Module.End R M) (μ : R),
  f.HasEigenvalue μ ↔ (LinearMap.charpoly f).IsRoot μ

The roots of the characteristic polynomial are exactly the eigenvalues. R is required to be an integral domain, otherwise there is the counterexample: R = M = Z/6Z, f(x) = 2x, v = 3, μ = 4, but p = X - 2.

Defined in

Mathlib.LinearAlgebra.Eigenspace.Charpoly

Cited by

1 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainAddCommGroupModuleModule.FreeModule.Finite