Cross products

This module defines the cross product of vectors in $R^3$ for $R$ a commutative ring, as a bilinear map.

Main definitions

• crossProduct is the cross product of pairs of vectors in $R^3$.

Main results

• triple_product_eq_det
• cross_dot_cross
• jacobi_cross

Notation

The scope Matrix gives the following notation:

• ⨯₃ for the cross product

Tags

cross product

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

The cross product of two vectors in $R^3$ for $R$ a commutative ring.

Equations

• crossProduct = LinearMap.mk₂ R (fun (a b : Fin 3 → R) => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]) ⋯ ⋯ ⋯ ⋯

def Matrix.«term_⨯₃_» : Lean.TrailingParserDescr

The cross product of two vectors in $R^3$ for $R$ a commutative ring.

Equations

• Matrix.«term_⨯₃_» = Lean.ParserDescr.trailingNode `Matrix.«term_⨯₃_» 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨯₃ ") (Lean.ParserDescr.cat `term 75))

@[deprecated Matrix.«term_⨯₃_» (since := "2025-07-11")]

def «term_×₃_» : Lean.TrailingParserDescr

A deprecated notation for ⨯₃.

Equations

• «term_×₃_» = Lean.ParserDescr.trailingNode `Matrix._root_.«term_×₃_» 74 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×₃ ") (Lean.ParserDescr.cat `term 75))

def elabDeprecatedCross : Lean.Elab.Term.TermElab

A deprecated notation for ⨯₃.

Equations

• One or more equations did not get rendered due to their size.

theorem cross_apply {R : Type u_1} [CommRing R] (a b : Fin 3 → R) : (crossProduct a) b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]

@[simp]

theorem cross_anticomm {R : Type u_1} [CommRing R] (v w : Fin 3 → R) : -(crossProduct v) w = (crossProduct w) v

theorem neg_cross {R : Type u_1} [CommRing R] (v w : Fin 3 → R) : -(crossProduct v) w = (crossProduct w) v

Alias of cross_anticomm.

@[simp]

theorem cross_anticomm' {R : Type u_1} [CommRing R] (v w : Fin 3 → R) : (crossProduct v) w + (crossProduct w) v = 0

@[simp]

theorem cross_self {R : Type u_1} [CommRing R] (v : Fin 3 → R) : (crossProduct v) v = 0

@[simp]

theorem dot_self_cross {R : Type u_1} [CommRing R] (v w : Fin 3 → R) : v ⬝ᵥ (crossProduct v) w = 0

The cross product of two vectors is perpendicular to the first vector.

@[simp]

theorem dot_cross_self {R : Type u_1} [CommRing R] (v w : Fin 3 → R) : w ⬝ᵥ (crossProduct v) w = 0

The cross product of two vectors is perpendicular to the second vector.

theorem triple_product_permutation {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) : u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u

Cyclic permutations preserve the triple product. See also triple_product_eq_det.

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

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

theorem cross_dot_cross {R : Type u_1} [CommRing R] (u v w x : Fin 3 → R) : (crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w

The scalar quadruple product identity, related to the Binet-Cauchy identity.

theorem leibniz_cross {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) : (crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)

The cross product satisfies the Leibniz lie property.

def Cross.lieRing {R : Type u_1} [CommRing R] : LieRing (Fin 3 → R)

The three-dimensional vectors together with the operations + and ⨯₃ form a Lie ring. Note we do not make this an instance as a conflicting one already exists via LieRing.ofAssociativeRing.

Equations

• Cross.lieRing = { toAddCommGroup := Pi.addCommGroup, bracket := fun (u v : Fin 3 → R) => (crossProduct u) v, add_lie := ⋯, lie_add := ⋯, lie_self := ⋯, leibniz_lie := ⋯ }

theorem cross_cross {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) : (crossProduct ((crossProduct u) v)) w = (crossProduct u) ((crossProduct v) w) - (crossProduct v) ((crossProduct u) w)

theorem jacobi_cross {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) : (crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) + (crossProduct w) ((crossProduct u) v) = 0

Jacobi identity: For a cross product of three vectors, their sum over the three even permutations is equal to the zero vector.

theorem crossProduct_ne_zero_iff_linearIndependent {F : Type u_2} [Field F] {v w : Fin 3 → F} : (crossProduct v) w ≠ 0 ↔ LinearIndependent F ![v, w]

theorem cross_cross_eq_smul_sub_smul {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) : (crossProduct ((crossProduct u) v)) w = (u ⬝ᵥ w) • v - (v ⬝ᵥ w) • u

The scalar triple product expansion of the vector triple product.

theorem cross_cross_eq_smul_sub_smul' {R : Type u_1} [CommRing R] (u v w : Fin 3 → R) : (crossProduct u) ((crossProduct v) w) = (u ⬝ᵥ w) • v - (v ⬝ᵥ u) • w

Alternative form of the scalar triple product expansion of the vector triple product.