genEigenrange_nat — Mathlib

English

When k is a natural number, genEigenrange μ k equals the range of (f − μ I)^k.

Русский

Если k ∈ ℕ, то genEigenrange μ k равно диапазону (f − μ I)^k.

LaTeX

$$genEigenrange f μ k = Range((f - μ·1)^k)$$

Lean4

theorem genEigenrange_nat {f : End R M} {μ : R} {k : ℕ} : f.genEigenrange μ k = LinearMap.range ((f - μ • 1) ^ k) :=
  by
  ext x
  simp only [genEigenrange, Nat.cast_le, Submodule.mem_iInf, LinearMap.mem_range]
  constructor
  · intro h
    exact h _ le_rfl
  · rintro ⟨x, rfl⟩ i hi
    have : k = i + (k - i) := by omega
    rw [this, pow_add]
    exact ⟨_, rfl⟩

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