English
For any matrices A,B, mulᵣ A B equals the standard matrix product A B.
Русский
Для любых матриц A,B, mulᵣ A B равно стандартному произведению матриц A B.
LaTeX
$$$A.mulᵣ B = A B$$$
Lean4
/-- This can be used to prove
```lean
example [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₂₂] :=
(mulᵣ_eq _ _).symm
```
-/
@[simp]
theorem mulᵣ_eq [Mul α] [AddCommMonoid α] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) :
mulᵣ A B = A * B := by
simp [mulᵣ, Matrix.transpose]
rfl