pow_apply

Mathlib.LinearAlgebra.Eigenspace.Basic

URI: https://scilib.ai/kg/mathlib#Module.End.HasEigenvector.pow_apply

English

If v is an eigenvector for μ then (f^n) v = μ^n v for all n.

Русский

Если v — эйгенвектор, то для любого n выполняется (f^n) v = μ^n v.

LaTeX

$$If hv: HasEigenvector f μ v, then ∀ n ∈ ℕ, (f^n) v = μ^n v.$$

Lean4

nonrec theorem pow_apply {f : End R M} {μ : R} {v : M} (hv : f.HasEigenvector μ v) (n : ℕ) : (f ^ n) v = μ ^ n • v :=
  hv.pow_apply n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru