English
If Z is nonzero and P,Q lie on W with P0 Q2 ≠ Q0 P2, then addXYZ(P,Q) equals addZ(P,Q) times the 3-vector whose entries are the affine coordinates: [X_affine, Y_affine, 1], with X_affine,Y_affine given by the affine addition formulas.
Русский
Если Z ненулевой и P,Q лежат на W, с P0 Q2 ≠ Q0 P2, то addXYZ(P,Q) = addZ(P,Q) · [X_affine, Y_affine, 1], где X_affine,Y_affine — аффинные формулы сложения.
LaTeX
$$$\mathrm{addXYZ}(P,Q) = \mathrm{addZ}(P,Q) \cdot \begin{pmatrix} \mathrm{toAffine.addX}(P_x/P_z, Q_x/Q_z, P_y/P_z, \mathrm{slope}) \\ \mathrm{toAffine.addY}(P_x/P_z, Q_x/Q_z, P_y/P_z, \mathrm{slope}) \\ 1 \end{pmatrix}$$$
Lean4
theorem addXYZ_of_Z_ne_zero [DecidableEq F] {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
(hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) :
W.addXYZ P Q =
W.addZ P Q •
![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
(W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
1] :=
by
have hZ : IsUnit <| W.addZ P Q := isUnit_addZ_of_X_ne hP hQ hx
erw [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, ← addY_of_Z_ne_zero hP hQ hPz hQz hx,
hZ.mul_div_cancel, mul_one]
