toMatrix_pow — Mathlib

English

For a linear map f: M1→M1 and k ∈ N, the k-th power of its matrix equals the matrix of f^k: (toMatrix v1 v1 f)^k = toMatrix v1 v1 (f^k).

Русский

Для линейного отображения f: M1→M1 и натурального k, матрица f^k равна k-й степени матрицы f: (toMatrix v1 v1 f)^k = toMatrix v1 v1 (f^k).

LaTeX

$$$\big( \mathrm{toMatrix}_{v_1,v_1}(f) \big)^k = \mathrm{toMatrix}_{v_1,v_1}(f^k)$$$

Lean4

theorem toMatrix_pow (f : M₁ →ₗ[R] M₁) (k : ℕ) : (toMatrix v₁ v₁ f) ^ k = toMatrix v₁ v₁ (f ^ k) := by
  induction k with
  | zero => simp
  | succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]

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