mulVec_replicateCol_eq_const — Mathlib

English

For finite m and α a nonunital nonassociative semiring, with v, w ∈ α^m, v ᵥ* replicateCol ι w = Function.const_{ι} (v ⬝ᵥ w).

Русский

Для конечного m и α без единицы, для v, w ∈ α^m, верно: v ᵥ* replicateCol ι w = Function.const_{ι} (v ⬝ᵥ w).

LaTeX

$$$ v ᵥ* replicateCol ι w = \mathrm{Function.const}_{ι} (v ⬝ᵥ w) $$$

Lean4

theorem mulVec_replicateCol_eq_const [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :
    v ᵥ* replicateCol ι w = Function.const _ (v ⬝ᵥ w) :=
  rfl

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