English
For a suitable semiring, mulVecᵣ equals the standard row-vector times matrix product: mulVecᵣ A v = A * v.
Русский
При подходящем полупрямоугольнике mulVecᵣ равняется стандартному произведению строки на матрицу: mulVecᵣ A v = A * v.
LaTeX
$$$\\text{mulVec}ᵣ\\; A\\; v = A \\; *\\; v$$$
Lean4
/-- This can be used to prove
```lean
example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
!![a₁₁, a₁₂;
a₂₁, a₂₂] *ᵥ ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
(mulVecᵣ_eq _ _).symm
```
-/
@[simp]
theorem mulVecᵣ_eq [NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α) :
mulVecᵣ A v = A *ᵥ v := by
simp [mulVecᵣ]
rfl
