English
If Z is nonzero, then the 3-coordinate of 2P is obtained by multiplying W'.dblZ(P) with the affine vector whose first two components are the affine additions involving X and Y coordinates, and whose last component is 1.
Русский
Если Z ≠ 0, то 2P задаётся как произведение W'.dblZ(P) на аффинный вектор, первый и второй компоненты которого выражаются через X и Y координаты, третий компонент равен 1.
LaTeX
$$$W'.\\mathrm{dblXYZ}(P) = W'.\\mathrm{dblZ}(P) \\cdot \\Big( \\big( W'.\\mathrm{toAffine}.\\mathrm{addX}(...) \\big), \\big( W'.\\mathrm{toAffine}.\\mathrm{addY}(...) \\big), 1 \\Big)$$$
Lean4
theorem dblXYZ_of_Y_eq {P Q : Fin 3 → F} (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
(hy : P y * Q z ^ 3 = Q y * P z ^ 3) (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) :
W.dblXYZ P = W.dblU P • ![1, 1, 0] := by erw [dblXYZ_of_Y_eq' hQz hx hy hy', smul_fin3, mul_one, mul_one, mul_zero]
