hasEigenvalue_iff_isRoot — Mathlib

English

f has eigenvalue μ if and only if μ is a root of the minimal polynomial of f.

Русский

f имеет собственный вектор с eigenvalue μ тогда и только тогда, когда μ является корнем минимального полинома f.

LaTeX

$$$$ f \text{ has eigenvalue } \mu \iff (\minpoly_R f) \text{ has root } \mu. $$$$

Lean4

theorem hasEigenvalue_iff_isRoot : f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ :=
  ⟨isRoot_of_hasEigenvalue, hasEigenvalue_of_isRoot⟩

Похожие утверждения