add_vecMulVec — Mathlib

English

For a commutative magma α, the transpose of vecMulVec w v equals vecMulVec v w.

Русский

Пусть α коммутативная магма; транспонирование vecMulVec w v дает vecMulVec v w.

LaTeX

$$(\\mathrm{vecMulVec} \\; w \\; v)^T = \\mathrm{vecMulVec} \\; v \\; w$$

Lean4

theorem add_vecMulVec [Mul α] [Add α] [RightDistribClass α] (w₁ w₂ : m → α) (v : n → α) :
    vecMulVec (w₁ + w₂) v = vecMulVec w₁ v + vecMulVec w₂ v :=
  ext fun _ _ => add_mul _ _ _

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