toLin'_pow — Mathlib

English

For any square matrix M, the linear map associated to M^k is the k-th power of the linear map associated to M.

Русский

Для любой квадратной матрицы M отображение, сопряжённое с M^k, равно k-ой степени отображения, сопряжённого с M.

LaTeX

$$$ (M^k).toLin' = M.toLin' ^ k $$$

Lean4

@[simp]
theorem toLin'_pow (M : Matrix n n R) (k : ℕ) : (M ^ k).toLin' = M.toLin' ^ k := by
  induction k with
  | zero => simp [End.one_eq_id]
  | succ n ih => rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]

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