maxGenEigenspace_eq_maxGenEigenspace_zero

English

An equality of maximal generalized eigenspace with a shifted operator: maxGenEigenspace f μ = maxGenEigenspace (f − μ I) 0.

Русский

Равенство максимального обобщённого эйгенпространства при сдвиге оператора: maxGenEigenspace f μ = maxGenEigenspace (f − μ I) 0.

LaTeX

$$$\\maxGenEigenspace(f, \\mu) = \\maxGenEigenspace\\big(f - \\mu I, \\; 0\\big).$$$

Lean4

theorem maxGenEigenspace_eq_maxGenEigenspace_zero (f : End R M) (μ : R) :
    maxGenEigenspace f μ = maxGenEigenspace (f - μ • 1) 0 := by ext; simp

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