trace_vecMulVec

Mathlib.LinearAlgebra.Matrix.Trace

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

← MathLib Explorer

English

For vectors a,b, tr(vecMulVec(a,b)) = a · b (dot product).

Русский

Для векторов a,b, tr(vecMulVec(a,b)) = a · b (скалярное произведение).

LaTeX

$$$$ \operatorname{tr}( \operatorname{vecMulVec}(a, b) ) = a \cdot b $$$$

Lean4

@[simp]
theorem trace_vecMulVec [NonUnitalNonAssocSemiring R] (a b : n → R) : trace (vecMulVec a b) = a ⬝ᵥ b := by
  rw [vecMulVec_eq Unit, trace_replicateCol_mul_replicateRow]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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