Low dimensions

DefinitionCross product#

The cross product of two vectors in \(R^3\) for \(R\) a commutative ring.

crossProduct.{u_1} {R : Type u_1} [CommRing R] : (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R

Sources

• Mathlib documentation: crossProduct
• Source of crossProduct in Mathlib/LinearAlgebra/CrossProduct.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Low dimensions

MathlibcrossProduct

Uses 3 · Used by 1

Statement usesAssociative algebra over a commutative ring · Integer · Linear map

Used byTriple product

TheoremTriple product#

The triple product of u, v, and w is equal to the determinant of the matrix with those vectors as its rows.

triple_product_eq_det.{u_1} {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) :
  u ⬝ᵥ (crossProduct v) w = Matrix.det ![u, v, w]

Sources

• Mathlib documentation: triple_product_eq_det
• Source of triple_product_eq_det in Mathlib/LinearAlgebra/CrossProduct.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Low dimensions

Mathlibtriple_product_eq_det

Uses 2

Statement usesCross product · Determinant

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.