English
If P and Q lie on the curve and P_x Q_z = Q_x P_z, then negAddY(P,Q) vanishes under a suitable normalization with (P_z Q_z)^2.
Русский
Если P и Q лежат на кривой и P_x Q_z = Q_x P_z, то negAddY(P,Q) обнуляется при нормализации на (P_z Q_z)^2.
LaTeX
$$$W'.negAddY(P,Q) (P_z Q_z)^2 = 0 \quad\text{если } P_x Q_z = Q_x P_z$$$
Lean4
theorem negAddY_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
W.negAddY P Q =
((P y * Q z - Q y * P z) *
((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
P y * Q z * (P x * Q z - Q x * P z) ^ 3) /
(P z * Q z) ^ 2 :=
by rw [← negAddY_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]
