English
If P1,P2 are nonsingular points with P1 ≠ P2 and the equation of addition holds, and the derivative of addPolynomial at x3 is nonzero, then the sum P1+P2 is nonsingular.
Русский
Если точки P1 и P2 невырожденные и не совпадают по x, и выполняется уравнение сложения, а производная addPolynomial в точке x3 не равна нулю, то сумма P1+P2 невырожденна.
LaTeX
$$Nonsingular at (W'.addX x1 x2 ℓ) (W'.negAddY x1 x2 y1 ℓ) provided hx' and (W'.addPolynomial x1 y1 ℓ).derivative.eval (W'.addX x1 x2 ℓ) ≠ 0.$$
Lean4
theorem nonsingular_negAdd_of_eval_derivative_ne_zero {x₁ x₂ y₁ ℓ : R}
(hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ))
(hx : (W'.addPolynomial x₁ y₁ ℓ).derivative.eval (W'.addX x₁ x₂ ℓ) ≠ 0) :
W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) :=
by
rw [Nonsingular, and_iff_right hx', negAddY, polynomialX, polynomialY]
eval_simp
contrapose! hx
rw [addPolynomial, linePolynomial, polynomial]
eval_simp
derivative_simp
simp only [zero_add, add_zero, sub_zero, zero_mul, mul_one]
eval_simp
linear_combination (norm := (norm_num1; ring1)) hx.left + ℓ * hx.right
