English
The k-th power of the left-multiplication map by a equals the left-multiplication map by a^k: (mulLeftLinearMap n R a)^k = mulLeftLinearMap n R (a^k).
Русский
Степень k от отображения левого умножения на A равна отображению левого умножения на A^k: (L_A)^k = L_{A^k}.
LaTeX
$$$\big(\operatorname{mulLeftLinearMap} n\ R\ a\big)^{k} = \operatorname{mulLeftLinearMap} n\ R\ (a^{k})$$$
Lean4
/-- A version of `LinearMap.pow_mulLeft` for matrix multiplication. -/
@[simp]
theorem pow_mulLeftLinearMap (a : Matrix m m A) (k : ℕ) : mulLeftLinearMap n R a ^ k = mulLeftLinearMap n R (a ^ k) :=
match k with
| 0 => by rw [pow_zero, pow_zero, mulLeftLinearMap_one, Module.End.one_eq_id]
| (n + 1) => by rw [pow_succ, pow_succ, mulLeftLinearMap_mul, Module.End.mul_eq_comp, pow_mulLeftLinearMap]
