English
Let A = [a11 a12; a21 a22] and B = [b11 b12; b21 b22]. Then AB equals the 2×2 matrix with entries a11 b11 + a12 b21, a11 b12 + a12 b22, a21 b11 + a22 b21, a21 b12 + a22 b22.
Русский
Пусть A = [a11 a12; a21 a22] и B = [b11 b12; b21 b22]. Тогда AB равно матрице 2×2 со следующими элементами: a11 b11 + a12 b21, a11 b12 + a12 b22, a21 b11 + a22 b21, a21 b12 + a22 b22.
LaTeX
$$$\begin{pmatrix} a_{11} & a_{12} \\ a_{21} & a_{22} \end{pmatrix} \begin{pmatrix} b_{11} & b_{12} \\ b_{21} & b_{22} \end{pmatrix} = \begin{pmatrix} a_{11} b_{11} + a_{12} b_{21} & a_{11} b_{12} + a_{12} b_{22} \\ a_{21} b_{11} + a_{22} b_{21} & a_{21} b_{12} + a_{22} b_{22} \end{pmatrix}$$$
Lean4
theorem mul_fin_two [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂] =
!![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] :=
by
ext i j
fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, Fin.sum_univ_succ]
