replicateRow_mul_replicateCol_apply

English

For m finite and α with Mul and AddCommMonoid structure, (replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w.

Русский

Пусть m конечно; для любых v, w: m → α и i, j соответствующих индексов, элемент на позиции (i,j) равен v ⬝ᵥ w.

LaTeX

$$$ (\mathrm{replicateRow}\ ι\ v \; * \; \mathrm{replicateCol}\ ι\ w)\ i j = v ⬝ᵥ w $$$

Lean4

@[simp]
theorem replicateRow_mul_replicateCol_apply [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) (i j) :
    (replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w :=
  rfl

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