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