jacobi_cross — Mathlib

English

The sum of cross products over even permutations vanishes (Jacobi identity for the cross product).

Русский

Сумма попарно перемещённых по чётным перестановкам произведений равна нулю (идентичность Якоби).

LaTeX

$$$u \\times (v \\times w) + v \\times (w \\times u) + w \\times (u \\times v) = 0$$$

Lean4

/-- **Jacobi identity**: For a cross product of three vectors,
their sum over the three even permutations is equal to the zero vector. -/
theorem jacobi_cross (u v w : Fin 3 → R) : u ⨯₃ (v ⨯₃ w) + v ⨯₃ (w ⨯₃ u) + w ⨯₃ (u ⨯₃ v) = 0 :=
  lie_jacobi u v w

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