pow — Mathlib

English

If f has uniform eigenvalue μ at index 1, then for any natural n, (f^n) has uniform eigenvalue μ^n at index 1.

Русский

Если f имеет унифицированное собственное значение μ при индексе 1, тогда для любого n ∈ ℕ, (f^n) имеет унифицированное собственное значение μ^n при индексе 1.

LaTeX

$$$f.HasUnifEigenvalue μ 1 \rightarrow (f^n).HasUnifEigenvalue (μ^n) 1$ for all n ∈ ℕ$$

Lean4

theorem pow {f : End R M} {μ : R} (h : f.HasUnifEigenvalue μ 1) (n : ℕ) : (f ^ n).HasUnifEigenvalue (μ ^ n) 1 :=
  by
  rw [HasUnifEigenvalue, Submodule.ne_bot_iff]
  obtain ⟨m : M, hm⟩ := h.exists_hasUnifEigenvector
  exact ⟨m, by simpa [mem_genEigenspace_one] using hm.pow_apply n, hm.2⟩

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