val

Mathlib.LinearAlgebra.Eigenspace.Basic

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

English

The eigenvalues of f form a distinguished type (the set of μ for which μ is an eigenvalue of f).

Русский

Множество собственных значений эндоморфизма f образует тип (подмножество μ, для которых μ является eigenvalue).

LaTeX

$$Eigenvalues(f) := { μ ∈ R | HasEigenvalue(f, μ) }$$

Lean4

@[coe]
abbrev val (f : Module.End R M) : Eigenvalues f → R :=
  UnifEigenvalues.val f 1

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

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

Разделы

Аффилиация

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