replicateCol_vecMul — Mathlib

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

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