replicateRow_vecMul — Mathlib

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

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