Cross products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Notation #

The locale matrix gives the following notation:

×₃ for the cross product

Tags #

crossproduct

source

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 = linear_map.mk₂ R (λ (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_4 cross_product._proof_5 cross_product._proof_6 cross_product._proof_7

source

theorem cross_apply {R : Type u_1} [comm_ring R] (a b : fin 3 → R) :

⇑(⇑cross_product 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]

source

@[simp]

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

-⇑(⇑cross_product v) w = ⇑(⇑cross_product w) v

source

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

-⇑(⇑cross_product v) w = ⇑(⇑cross_product w) v

Alias of cross_anticomm.

source

@[simp]

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

⇑(⇑cross_product v) w + ⇑(⇑cross_product w) v = 0

source

@[simp]

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

⇑(⇑cross_product v) v = 0

source

@[simp]

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

matrix.dot_product v (⇑(⇑cross_product v) w) = 0

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

source

@[simp]

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

matrix.dot_product w (⇑(⇑cross_product v) w) = 0

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

source

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

matrix.dot_product u (⇑(⇑cross_product v) w) = matrix.dot_product v (⇑(⇑cross_product w) u)

Cyclic permutations preserve the triple product. See also triple_product_eq_det.

source

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

matrix.dot_product u (⇑(⇑cross_product 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.

source

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

matrix.dot_product (⇑(⇑cross_product u) v) (⇑(⇑cross_product w) x) = matrix.dot_product u w * matrix.dot_product v x - matrix.dot_product u x * matrix.dot_product v w

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

source

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

⇑(⇑cross_product u) (⇑(⇑cross_product v) w) = ⇑(⇑cross_product (⇑(⇑cross_product u) v)) w + ⇑(⇑cross_product v) (⇑(⇑cross_product u) w)

The cross product satisfies the Leibniz lie property.

source

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

cross.lie_ring = {to_add_comm_group := {add := add_comm_group.add pi.add_comm_group, add_assoc := _, zero := add_comm_group.zero pi.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul pi.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg pi.add_comm_group, sub := add_comm_group.sub pi.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul pi.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, to_has_bracket := {bracket := λ (u v : fin 3 → R), ⇑(⇑cross_product u) v}, add_lie := _, lie_add := _, lie_self := _, leibniz_lie := _}

source

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

⇑(⇑cross_product (⇑(⇑cross_product u) v)) w = ⇑(⇑cross_product u) (⇑(⇑cross_product v) w) - ⇑(⇑cross_product v) (⇑(⇑cross_product u) w)

source

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

⇑(⇑cross_product u) (⇑(⇑cross_product v) w) + ⇑(⇑cross_product v) (⇑(⇑cross_product w) u) + ⇑(⇑cross_product w) (⇑(⇑cross_product 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.