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 #
Notation #
The locale matrix
gives the following notation:
×₃
for the cross product
Tags #
crossproduct
The cross product of two vectors in $R^3$ for $R$ a commutative ring.
Alias of cross_anticomm
.
The cross product of two vectors is perpendicular to the first vector.
The cross product of two vectors is perpendicular to the second vector.
Cyclic permutations preserve the triple product. See also triple_product_eq_det
.
The triple product of u
, v
, and w
is equal to the determinant of the matrix
with those vectors as its rows.
The scalar quadruple product identity, related to the Binet-Cauchy identity.
The cross product satisfies the Leibniz lie property.
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 := _}
Jacobi identity: For a cross product of three vectors, their sum over the three even permutations is equal to the zero vector.