English
For non-unital semirings, vecMulᵣ v A = v ᵥ* A, i.e., the right-acting vector multiplication coincides with the standard row-vector product.
Русский
Для неединичного полупкольца vecMulᵣ v A равно v ᵥ* A, то есть совпадает с обычным произведением строки на матрицу.
LaTeX
$$$\\text{vecMul}ᵣ\\; v\\; A = v \\\\ ᵥ*\\; A$$$
Lean4
/-- This can be used to prove
```lean
example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
![b₁, b₂] ᵥ* !![a₁₁, a₁₂;
a₂₁, a₂₂] = ![b₁*a₁₁ + b₂*a₂₁, b₁*a₁₂ + b₂*a₂₂] :=
(vecMulᵣ_eq _ _).symm
```
-/
@[simp]
theorem vecMulᵣ_eq [NonUnitalNonAssocSemiring α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α) :
vecMulᵣ v A = v ᵥ* A := by
simp [vecMulᵣ]
rfl
