dot_self_cross — Mathlib

English

The triple product equals the determinant of the matrix formed by the three vectors as rows.

Русский

Тройной произведение равно детерминанту матрицы, построенной из трёх векторов как строк.

LaTeX

$$$u \\cdot (v \\times w) = \\det \\begin{pmatrix} u \\\\ v \\\\ w \\end{pmatrix}$$$

Lean4

/-- The cross product of two vectors is perpendicular to the first vector. -/
@[simp]
theorem dot_self_cross (v w : Fin 3 → R) : v ⬝ᵥ v ⨯₃ w = 0 :=
  by
  rw [cross_apply, vec3_dotProduct]
  dsimp only [Matrix.cons_val]
  ring

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