mapsTo_maxGenEigenspace_of_comm — Mathlib

English

If f and g commute, then g maps the maximal generalized eigenspace for f into itself, i.e., maps to f.maxGenEigenspace μ.

Русский

Если f и g коммутируют, то g отображает максимальное обобщённое эйгенпространство f на себя: g( maxGenEigenspace μ ) ⊆ maxGenEigenspace μ.

LaTeX

$$$g \\text{ commutes with } f \\Rightarrow g\\bigl(\\maxGenEigenspace(f, μ)\\bigr) \\subseteq \\maxGenEigenspace(f, μ).$$$

Lean4

theorem mapsTo_maxGenEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) :
    MapsTo g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
  mapsTo_genEigenspace_of_comm h μ ⊤

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