hasEigenvalue_of_hasEigenvector

Mathlib.LinearAlgebra.Eigenspace.Basic

URI: https://scilib.ai/kg/mathlib#Module.End.hasEigenvalue_of_hasEigenvector

English

If x is an eigenvector for μ (HasEigenvector f μ x), then μ is an eigenvalue (HasEigenvalue f μ).

Русский

Если x — эйгенвектор для μ, то μ — собственное значение.

LaTeX

$$HasEigenvector(f, μ, x) ⇒ HasEigenvalue(f, μ)$$

Lean4

theorem hasEigenvalue_of_hasEigenvector {f : End R M} {μ : R} {x : M} (h : HasEigenvector f μ x) : HasEigenvalue f μ :=
  h.hasUnifEigenvalue

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru