triple_product_eq_det — Mathlib

English

The triple product equals the determinant of the matrix with the three vectors as its rows.

Русский

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

LaTeX

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

Lean4

/-- The triple product of `u`, `v`, and `w` is equal to the determinant of the matrix
with those vectors as its rows. -/
theorem triple_product_eq_det (u v w : Fin 3 → R) : u ⬝ᵥ v ⨯₃ w = Matrix.det ![u, v, w] :=
  by
  rw [vec3_dotProduct, cross_apply, det_fin_three]
  dsimp only [Matrix.cons_val]
  ring

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