genEigenspace_le_smul — Mathlib

English

For endomorphism f, scaling by t yields (f.genEigenspace μ k) ≤ (t f).genEigenspace (t μ) k.

Русский

Умножение на t линейного отображения даёт вложение соответствующих обобщённых эйгенпространств: E_{μ} ⊆ E_{tμ}^{t f}.

LaTeX

$$$ (f.genEigenspace \\mu k) \\le (t \\cdot f).genEigenspace (t \\mu) k $$$

Lean4

theorem genEigenspace_le_smul (f : Module.End R M) (μ t : R) (k : ℕ∞) :
    (f.genEigenspace μ k) ≤ (t • f).genEigenspace (t * μ) k :=
  by
  intro m hm
  simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢
  peel hm with l hlk hl
  rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]

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