English
If two points P1 and P2 are nonsingular on W and their addition is well-defined (not a vertical line), then the sum is nonsingular.
Русский
Если две точки P1 и P2 невырождены на кривой W и их сложение определено (не вертикальная прямая), то сумма невырожденна.
LaTeX
$$W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))$$
Lean4
theorem nonsingular_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
W.Nonsingular (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.negAddY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
by
by_cases hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
· rwa [negAddY, hx₁, sub_self, mul_zero, zero_add]
· by_cases hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
· by_cases hx : x₁ = x₂
· subst hx
contradiction
·
rwa [negAddY, ← neg_sub, mul_neg, hx₂, slope_of_X_ne hx, div_mul_cancel₀ _ <| sub_ne_zero_of_ne hx, neg_sub,
sub_add_cancel]
· apply nonsingular_negAdd_of_eval_derivative_ne_zero <| equation_negAdd h₁.left h₂.left hxy
rw [derivative_addPolynomial_slope h₁.left h₂.left hxy]
eval_simp
simp only [neg_ne_zero, sub_self, mul_zero, add_zero]
exact mul_ne_zero (sub_ne_zero_of_ne hx₁) (sub_ne_zero_of_ne hx₂)
