cross_anticomm' — Mathlib

English

The dot of a vector with the cross product of itself with another is zero, expressing perpendicularity.

Русский

Скалярное произведение вектора на cross вектора, полученного из него и другого вектора, равно нулю.

LaTeX

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

Lean4

@[simp]
theorem cross_anticomm' (v w : Fin 3 → R) : v ⨯₃ w + w ⨯₃ v = 0 := by rw [add_eq_zero_iff_eq_neg, cross_anticomm]

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