triple_product_permutation — Mathlib

English

Cyclic permutations preserve the scalar triple product: uᵀ(v×w) = vᵀ(w×u).

Русский

Циклические перестановки сохраняют скалярное тройное произведение: u · (v × w) = v · (w × u).

LaTeX

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

Lean4

/-- Cyclic permutations preserve the triple product. See also `triple_product_eq_det`. -/
theorem triple_product_permutation (u v w : Fin 3 → R) : u ⬝ᵥ v ⨯₃ w = v ⬝ᵥ w ⨯₃ u :=
  by
  simp_rw [cross_apply, vec3_dotProduct]
  dsimp only [Matrix.cons_val]
  ring

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