Vectors with vanishing cross product

Complements to Mathlib.LinearAlgebra.CrossProduct. Over a field, two nonzero vectors of K³ have vanishing cross product exactly when they are proportional (Projectivization.mk_eq_mk_iff_crossProduct_eq_zero). Over a commutative ring R, the coordinates of v ⨯₃ w are the 2 × 2 minors of the matrix with rows v and w, and when they vanish and both vectors have a unit coordinate, v is a unit multiple of w.

Main results

• TauCeti.exists_eq_units_smul_of_crossProduct_eq_zero: if v ⨯₃ w = 0 and v and w each have a unit coordinate, then v = u • w for a unit u.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/AdditionChartGlue.lean: ratio_eq_of_minor and isUnit_of_minor, combined as exists_eq_units_smul_of_crossProduct_eq_zero. Here the vanishing of the 2 × 2 minors is stated as the vanishing of the cross product.

theorem TauCeti.exists_eq_units_smul_of_crossProduct_eq_zero {R : Type u_1} [CommRing R] {v w : Fin 3 → R} (h : (crossProduct v) w = 0) {k l : Fin 3} (hv : IsUnit (v k)) (hw : IsUnit (w l)) : ∃ (u : Rˣ), v = u • w

Let v and w be vectors of R³, over a commutative ring R, each with a unit coordinate. If v ⨯₃ w = 0, then v is a unit multiple of w.