replicateRow_mulVec — Mathlib

English

Let Fintype n and α a nonunital nonassociative semiring. For M ∈ M(m, n, α) and v ∈ α^n, replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ.

Русский

Пусть Fintype n и α — полукольцо без единицы. Для M ∈ M(m, n, α) и v ∈ α^n, replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ.

LaTeX

$$$ \mathrm{replicateRow}\ ι\ (M *ᵥ v) = (M * \mathrm{replicateCol}\ ι\ v)^T $$$

Lean4

theorem replicateRow_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
    replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ := by
  ext
  rfl

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