dot_cross_self — Mathlib

English

The cross product is orthogonal to the second vector in the triple product, and related symmetry holds.

Русский

Векторное произведение ортогонально указанному вектору в тройном произведении; соблюдаются соответствующие симметрии.

LaTeX

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

Lean4

/-- The cross product of two vectors is perpendicular to the second vector. -/
@[simp]
theorem dot_cross_self (v w : Fin 3 → R) : w ⬝ᵥ v ⨯₃ w = 0 := by
  rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]

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