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