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