replicateCol_mulVec — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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