English
Let R be a commutative ring and u, v, w be elements of R^3. Then u × (v × w) = (u · w) v − (u · v) w, i.e., the scalar triple expansion for the vector triple product.
Русский
Пусть R — коммутативное кольцо, и v, w, u — элементы R^3. Тогда u × (v × w) = (u · w) v − (u · v) w, то есть формула разложения скалярного триплетного произведения.
LaTeX
$$$u \\times_3 (v \\times_3 w) = (u \\cdot w)\\, v - (u \\cdot v)\\, w$$$
Lean4
/-- Alternative form of the scalar triple product expansion of the vector triple product. -/
theorem cross_cross_eq_smul_sub_smul' (u v w : Fin 3 → R) : u ⨯₃ (v ⨯₃ w) = (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w :=
by
simp_rw [cross_apply, vec3_dotProduct]
ext i
fin_cases i <;>
· simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, cons_val, cons_val_one, cons_val_zero,
Fin.reduceFinMk, Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
ring
