English
For nonsingular points P1 = (x1, y1) and P2 = (x2, y2) with x1,y1 and x2,y2 nonsingular and not vertically aligned (no P1 + P2 = ∞ on a vertical line), the product of their XYIdeal' classes equals the XYIdeal' class of the sum P1 + P2: [XYIdeal'(h1)] · [XYIdeal'(h2)] = [XYIdeal'(nonsingular_add h1 h2 hxy)].
Русский
Для двух невырожденных точек P1 и P2, не лежащих на одной вертикали, произведение классов XYIdeal' соответствует классу XYIdeal' точки P1 + P2: [XYIdeal'(P1)]·[XYIdeal'(P2)] = [XYIdeal'(P1+P2)].
LaTeX
$$$[XYIdeal'(h_1)]\\cdot[XYIdeal'(h_2)]=[XYIdeal'(nonsingular\\_add\\, h_1\\, h_2\\, hxy)]$$$
Lean4
theorem mk_XYIdeal'_mul_mk_XYIdeal' [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁)
(h₂ : W.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) = ClassGroup.mk (XYIdeal' <| nonsingular_add h₁ h₂ hxy) :=
by
rw [← map_mul]
exact
(ClassGroup.mk_eq_mk_of_coe_ideal (coeIdeal_mul ..).symm <| XYIdeal'_eq _).mpr
⟨_, _, XClass_ne_zero _, YClass_ne_zero _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩
