vecMulVec_eq — Mathlib

English

For any α with Mul and AddCommMonoid, and Unique ι, vecMulVec w v = replicateCol ι w * replicateRow ι v.

Русский

Для любых w,v: m→α и Unique ι имеем vecMulVec w v = replicateCol ι w * replicateRow ι v.

LaTeX

$$$ vecMulVec\ w\ v = replicateCol\ ι\ w * replicateRow\ ι\ v $$$

Lean4

theorem vecMulVec_eq [Mul α] [AddCommMonoid α] [Unique ι] (w : m → α) (v : n → α) :
    vecMulVec w v = replicateCol ι w * replicateRow ι v :=
  by
  ext
  simp [vecMulVec, mul_apply]

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