English
The cross MK formula describes how the cross operation behaves on MK representatives depending on whether the cross product vanishes.
Русский
Формула MK-переменной описывает поведение операции cross на представителях MK в зависимости от того, обращается ли crossProduct в ноль.
LaTeX
$$$cross(\\text{mk}(F,v,hv), \\text{mk}(F,w,hw)) = \\begin{cases} \\text{mk}(F,v,hv), & \\text{if } crossProduct(v,w)=0 \\\\ \\text{mk}(F, crossProduct(v,w), h), & \\text{otherwise} \\end{cases}$$$
Lean4
/-- Cross product on the projective plane. -/
def cross : ℙ F (Fin 3 → F) → ℙ F (Fin 3 → F) → ℙ F (Fin 3 → F) :=
Quotient.map₂ (fun v w ↦ if h : crossProduct v.1 w.1 = 0 then v else ⟨crossProduct v.1 w.1, h⟩)
(fun _ _ ⟨a, ha⟩ _ _ ⟨b, hb⟩ ↦
by
simp_rw [← ha, ← hb, LinearMap.map_smul_of_tower, LinearMap.smul_apply, smul_smul, mul_comm b a,
smul_eq_zero_iff_eq]
split_ifs
· use a
· use a * b)
