transpose_vecMulVec

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#Matrix.transpose_vecMulVec

English

For commutative magma α, vecMulVec w v transposes to vecMulVec v w.

Русский

Для коммутативной магмы α vecMulVec w v обращается в vecMulVec v w.

LaTeX

$$vecMulVec w v^{T} = vecMulVec v w$$

Lean4

@[simp]
theorem transpose_vecMulVec [CommMagma α] (w : m → α) (v : n → α) : (vecMulVec w v)ᵀ = vecMulVec v w :=
  ext fun _ _ => mul_comm _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru