vecMulVec_add — Mathlib

English

For commutative magma α, the transpose swaps the two arguments of vecMulVec.

Русский

При коммутативной магме транспонирование меняет местами два аргумента vecMulVec.

LaTeX

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

Lean4

theorem vecMulVec_add [Mul α] [Add α] [LeftDistribClass α] (w : m → α) (v₁ v₂ : n → α) :
    vecMulVec w (v₁ + v₂) = vecMulVec w v₁ + vecMulVec w v₂ :=
  ext fun _ _ => mul_add _ _ _

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