mem_spectrum

Mathlib.LinearAlgebra.Eigenspace.Basic

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

English

If μ is an eigenvalue of f, then μ belongs to the spectrum of f.

Русский

Если μ является собственным значением f, то μ принадлежит спектру f.

LaTeX

$$HasEigenvalue(f, μ) ⇒ μ ∈ spectrum f$$

Lean4

nonrec theorem mem_spectrum {f : End R M} {μ : R} (hμ : HasEigenvalue f μ) : μ ∈ spectrum R f :=
  hμ.mem_spectrum

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

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

Разделы

Аффилиация

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