English
Under the Weierstrass projective setting, if P,Q lie on the curve and certain Y-equality constraints hold, then negDblY P equals the negative of dblU P in a suitable algebraic sense: negDblY P = -dblU P.
Русский
В проектной настройке Weierstrass, если P,Q лежат на кривой и выполняются условия по Y, то negDblY P = -dblU P.
LaTeX
$$$ {P Q: Fin 3 → F} (hP: W'.Equation P) (hQ: W'.Equation Q) \Rightarrow W'.negDblY P = - W'.dblU P$$$
Lean4
theorem negDblY_eq {P : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) :
W.negDblY P =
(-eval P W.polynomialX *
(eval P W.polynomialX ^ 2 - W.a₁ * eval P W.polynomialX * P z * (P y - W.negY P) -
W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
2 * P x * P z * (P y - W.negY P) ^ 2 -
P x * P z * (P y - W.negY P) ^ 2) +
P y * P z ^ 2 * (P y - W.negY P) ^ 3) /
P z ^ 2 :=
by rw [← negDblY_eq' hP, mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
