English
Let A ∈ Mat_{l×m}(R), B ∈ Mat_{m×n}(R) and x ∈ M1. Then Matrix.toLin v1 v3 (A B) x = (Matrix.toLin v2 v3 A)(Matrix.toLin v1 v2 B x).
Русский
Пусть A и B — матрицы соответствующих размеров и x ∈ M1. Тогда Matrix.toLin v1 v3 (A B) x = (Matrix.toLin v2 v3 A)(Matrix.toLin v1 v2 B x).
LaTeX
$$$\mathrm{toLin}_{v_1,v_3}(A B) x = \big( \mathrm{toLin}_{v_2,v_3}(A) \big) \Big( \mathrm{toLin}_{v_1,v_2}(B) x \Big)$$$
Lean4
@[simp]
theorem toLin_pow (A : Matrix n n R) (k : ℕ) : (A ^ k).toLin v₁ v₁ = (A.toLin v₁ v₁) ^ k := by
induction k with
| zero => simp only [pow_zero, toLin_one, End.one_eq_id]
| succ n ih => rw [pow_succ, pow_succ, toLin_mul v₁ v₁, ih, Module.End.mul_eq_comp]
