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 #
Notation #
The locale Matrix
gives the following notation:
×₃
for the cross product
Tags #
crossproduct
@[simp]
theorem
dot_self_cross
{R : Type u_1}
[CommRing R]
(v : Fin 3 → R)
(w : Fin 3 → R)
:
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 3 → R)
(w : Fin 3 → R)
:
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 3 → R)
(v : Fin 3 → R)
(w : Fin 3 → R)
:
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 3 → R)
(v : Fin 3 → R)
(w : Fin 3 → R)
:
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 3 → R)
(v : Fin 3 → R)
(w : Fin 3 → R)
(x : Fin 3 → R)
:
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.