eigenspace_div — Mathlib

English

Let f be a linear endomorphism of a vector space V over a field K. For any a, b ∈ K with b ≠ 0, the generalized eigen-space corresponding to a/b equals the kernel of b f − a Id. In symbols: E_{a/b}(f) = Ker(b f − a I).

Русский

Пусть f — линейное отображение V → V над полем K. Пусть a, b ∈ K и b ≠ 0. Обобщённое эйгенпространство, связанное с a/b, равно ядру отображения b f − a Id. То есть E_{a/b}(f) = Ker(b f − a Id).

LaTeX

$$$\\operatorname{eigenspace}(f, a/b) = \\ker\\bigl(b\,f - a\,\\mathrm{Id}_V\\bigr).$$$

Lean4

theorem eigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
    eigenspace f (a / b) = LinearMap.ker (b • f - algebraMap K (End K V) a) :=
  genEigenspace_div f a b hb

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