English
Let m be finite and α a nonunital nonassociative semiring. For any matrix M ∈ M(m, n, α) and v ∈ α^m, replication of the row vᵥ* M equals the product of replication of v with M: replicateRow ι (v ᵥ* M) = replicateRow ι v * M.
Русский
Пусть m конечно, α — полукольцо без единицы и без ассоциации. Для матрицы M размером m×n и вектора v ∈ α^m выполняется: replicateRow ι (v ᵥ* M) = replicateRow ι v * M.
LaTeX
$$$ \mathrm{replicateRow}\ ι\ (v ᵥ* M) = \mathrm{replicateRow}\ ι\ v \; * \; M $$$
Lean4
theorem replicateRow_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
replicateRow ι (v ᵥ* M) = replicateRow ι v * M := by
ext
rfl