pow_apply — Mathlib

English

If v is a HasUnifEigenvector μ 1 v, then for every natural n, (f^n) v = μ^n · v.

Русский

Если v является HasUnifEigenvector μ 1 v, то для любого натурального n выполняется (f^n) v = μ^n · v.

LaTeX

$$HasUnifEigenvector(f, μ, 1, v) ⇒ ∀ n : Nat, (f^n) v = μ^n · v$$

Lean4

theorem pow_apply {f : End R M} {μ : R} {v : M} (hv : f.HasUnifEigenvector μ 1 v) (n : ℕ) : (f ^ n) v = μ ^ n • v := by
  induction n <;> simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

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