English
For A,B,C ∈ M_n(α) and indices i,j ∈ {1,...,n}, the (i,j)-entry of A B C is the dot product of the i-th row of A with the vector B times the j-th column of C^T; equivalently (ABC)_{ij} = sum_k A_{ik} (BC)_{kj}.
Русский
Для матриц A,B,C ∈ M_n(α) и индексов i,j ∈ {1,...,n} элемент (i,j) произведения A B C равен скалярному произведению i-й строки A и вектора B, умноженного на j-й столбец C^T; то есть (ABC)_{ij} = ∑_k A_{ik} (BC)_{kj}.
LaTeX
$$$(ABC)_{ij} = \sum_k A_{ik} (BC)_{kj}$$$
Lean4
theorem mul_mul_apply [Fintype n] (A B C : Matrix n n α) (i j : n) : (A * B * C) i j = A i ⬝ᵥ B *ᵥ (Cᵀ j) :=
by
rw [Matrix.mul_assoc]
simp [mul_apply, dotProduct, mulVec]
