HasEigenvalue — Mathlib

English

A scalar μ is an eigenvalue of f if there exists a nonzero x with f x = μ x.

Русский

Скаляр μ является собственным значением f, если существует ненулевой вектор x, такой что f x = μ x.

LaTeX

$$HasEigenvalue(f, μ) := HasUnifEigenvalue(f, μ, 1)$$

Lean4

/-- A scalar `μ` is an eigenvalue for a linear map `f` if there are nonzero vectors `x`
such that `f x = μ • x`. (Def 5.5 of [axler2015]). -/
abbrev HasEigenvalue (f : End R M) (a : R) : Prop :=
  HasUnifEigenvalue f a 1

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