replicateRow_mulVec_eq_const — Mathlib

English

For a finite m and α a nonunital nonassociative semiring, with v, w ∈ α^m, replicateRow ι v *ᵥ w equals the constant function on ι with value v ⬝ᵥ w (dot product).

Русский

Для конечного m и α неединичного полускалярного полусгруппы, для векторов v, w ∈ α^m, replicateRow ι v *ᵥ w равно константной функции на ι со значением v ⬝ᵥ w.

LaTeX

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

Lean4

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

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