cross_cross — Mathlib

English

The triple product expands as a linear combination of the inputs with scalar coefficients obtained from dot products.

Русский

Тройное произведение разлагается как линейная комбинация входов со скалярами, получаемыми из скалярных произведений.

LaTeX

$$$u \\times v \\times w = (u \\cdot w) \\, v - (v \\cdot w) \\, u$$$

Lean4

theorem cross_cross (u v w : Fin 3 → R) : u ⨯₃ v ⨯₃ w = u ⨯₃ (v ⨯₃ w) - v ⨯₃ (u ⨯₃ w) :=
  lie_lie u v w

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