Documentation

Mathlib.LinearAlgebra.CrossProduct

Cross products #

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

Main definitions #

Main results #

Notation #

The locale Matrix gives the following notation:

Tags #

crossproduct

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

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

Instances For
    theorem cross_apply {R : Type u_1} [CommRing R] (a : Fin 3R) (b : Fin 3R) :
    ↑(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 : Fin 3R) (w : Fin 3R) :
    -↑(crossProduct v) w = ↑(crossProduct w) v
    theorem neg_cross {R : Type u_1} [CommRing R] (v : Fin 3R) (w : Fin 3R) :
    -↑(crossProduct v) w = ↑(crossProduct w) v

    Alias of cross_anticomm.

    @[simp]
    theorem cross_anticomm' {R : Type u_1} [CommRing R] (v : Fin 3R) (w : Fin 3R) :
    ↑(crossProduct v) w + ↑(crossProduct w) v = 0
    @[simp]
    theorem cross_self {R : Type u_1} [CommRing R] (v : Fin 3R) :
    ↑(crossProduct v) v = 0
    @[simp]
    theorem dot_self_cross {R : Type u_1} [CommRing R] (v : Fin 3R) (w : Fin 3R) :
    Matrix.dotProduct 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 : Fin 3R) (w : Fin 3R) :
    Matrix.dotProduct 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 : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
    Matrix.dotProduct u (↑(crossProduct v) w) = Matrix.dotProduct 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 : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
    Matrix.dotProduct 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 : Fin 3R) (v : Fin 3R) (w : Fin 3R) (x : Fin 3R) :
    Matrix.dotProduct (↑(crossProduct u) v) (↑(crossProduct w) x) = Matrix.dotProduct u w * Matrix.dotProduct v x - Matrix.dotProduct u x * Matrix.dotProduct v w

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

    theorem leibniz_cross {R : Type u_1} [CommRing R] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
    ↑(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 3R)

    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.

    Instances For
      theorem cross_cross {R : Type u_1} [CommRing R] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
      ↑(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 : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
      ↑(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.