cross_dot_cross — Mathlib

English

The scalar quadruple product identity relates two cross products and two dot products via a bilinear form formula.

Русский

Кватернионное тождество между двумя векторными произведениями и двумя скалярными произведениями через билинейную форму.

LaTeX

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

Lean4

/-- The scalar quadruple product identity, related to the Binet-Cauchy identity. -/
theorem cross_dot_cross (u v w x : Fin 3 → R) : u ⨯₃ v ⬝ᵥ w ⨯₃ x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w :=
  by
  simp_rw [cross_apply, vec3_dotProduct]
  dsimp only [Matrix.cons_val]
  ring

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