# mathlibdocumentation

linear_algebra.cross_product

# Cross products #

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

## Main definitions #

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

## Main results #

• triple_product_eq_det
• cross_dot_cross
• jacobi_cross

## Notation #

The locale matrix gives the following notation:

• ×₃ for the cross product

## Tags #

crossproduct

def cross_product {R : Type u_1} [comm_ring 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
• cross_product = (λ (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]) cross_product._proof_2 cross_product._proof_3 cross_product._proof_4 cross_product._proof_5
theorem cross_apply {R : Type u_1} [comm_ring R] (a b : fin 3 → R) :
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} [comm_ring R] (v w : fin 3 → R) :
- w = v
theorem neg_cross {R : Type u_1} [comm_ring R] (v w : fin 3 → R) :
- w = v

Alias of cross_anticomm.

@[simp]
theorem cross_anticomm' {R : Type u_1} [comm_ring R] (v w : fin 3 → R) :
w + v = 0
@[simp]
theorem cross_self {R : Type u_1} [comm_ring R] (v : fin 3 → R) :
v = 0
@[simp]
theorem dot_self_cross {R : Type u_1} [comm_ring R] (v w : fin 3 → R) :
( w) = 0

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

@[simp]
theorem dot_cross_self {R : Type u_1} [comm_ring R] (v w : fin 3 → R) :
( w) = 0

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

theorem triple_product_permutation {R : Type u_1} [comm_ring R] (u v w : fin 3 → R) :
( w) = ( u)

Cyclic permutations preserve the triple product. See also triple_product_eq_det.

theorem triple_product_eq_det {R : Type u_1} [comm_ring R] (u v w : fin 3 → R) :
( 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} [comm_ring R] (u v w x : fin 3 → R) :
( x) = -

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

theorem leibniz_cross {R : Type u_1} [comm_ring R] (u v w : fin 3 → R) :

The cross product satisfies the Leibniz lie property.

def cross.lie_ring {R : Type u_1} [comm_ring R] :
lie_ring (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 lie_ring.of_associative_ring`.

Equations
theorem cross_cross {R : Type u_1} [comm_ring R] (u v w : fin 3 → R) :
theorem jacobi_cross {R : Type u_1} [comm_ring R] (u v w : fin 3 → R) :
( w) + ( 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.