English
If P and Q lie on W and their z-coordinates are nonzero, then addX(P,Q) equals the explicit rational expression given by the same numerator over (Pz Qz)^2 times (Px Qz − Qx Pz).
Русский
Если P и Q лежат на W и их z-координаты не равны нулю, то addX(P,Q) равно явному рациональному выражению, заданному тем же числителем делённому на (Pz Qz)^2 и умноженному на (Px Qz − Qx Pz).
LaTeX
$$$W.addX(P,Q) = \dfrac{(P_y Q_z - Q_y P_z)^2 P_z Q_z + a_1 (P_y Q_z - Q_y P_z) P_z Q_z (P_x Q_z - Q_x P_z) - a_2 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_z Q_z)^2} (P_x Q_z - Q_x P_z),$$
Lean4
theorem addX_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
W.addX P Q =
((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 - Q x * P z) /
(P z * Q z) ^ 2 :=
by rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]
