leibniz_cross — Mathlib

English

The cross product satisfies the Leibniz rule with respect to the Lie bracket.

Русский

Векторное произведение удовлетворяет правилу Лейбница относительно скобки Ли.

LaTeX

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

Lean4

/-- The cross product satisfies the Leibniz lie property. -/
theorem leibniz_cross (u v w : Fin 3 → R) : u ⨯₃ (v ⨯₃ w) = u ⨯₃ v ⨯₃ w + v ⨯₃ (u ⨯₃ w) :=
  by
  simp_rw [cross_apply, vec3_add]
  apply vec3_eq <;> dsimp <;> ring

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