English
The cross product is a bilinear map from pairs of vectors in R^3 to R^3, giving a vector perpendicular to both inputs.
Русский
Векторное произведение задано как билинейное отображение из пары векторов в R^3 в R^3, дающее вектор, перпендикулярный обоим входным векторам.
LaTeX
$$$\\text{crossProduct} : (\\mathbb{R}^3) \\times (\\mathbb{R}^3) \\to \\mathbb{R}^3$, with components $([a,b,c] \\times [d,e,f])=(bf-ce, cd-af, ae-bd)$$$
Lean4
/-- The cross product of two vectors in $R^3$ for $R$ a commutative ring. -/
def crossProduct : (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R :=
by
apply LinearMap.mk₂ R fun 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]
· intros
simp_rw [vec3_add, Pi.add_apply]
apply vec3_eq <;> ring
· intros
simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]
· intros
simp_rw [vec3_add, Pi.add_apply]
apply vec3_eq <;> ring
· intros
simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]
