mulᵣ_eq — Mathlib

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

Похожие утверждения