English
For P, Q with P_z ≠ 0, Q_z ≠ 0 and nondegenerate Y-relations, adding scalar multiples obeys addU: addU(uP, vQ) = (uv)^2 · addU(P, Q).
Русский
При отсутствии нулевых Z и ненулевых Y-координатах, сумма скалярно умноженных точек удовлетворяет addU: addU(uP, vQ) = (uv)^2 · addU(P, Q).
LaTeX
$$$\\mathrm{addU}(u\\cdot P, v\\cdot Q) = (u v)^2 \\cdot \\mathrm{addU}(P,Q)$$$
Lean4
theorem dblXYZ_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 ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
W.dblXYZ P =
W.dblZ P •
![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
(W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
(W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
1] :=
by
have hZ {n : ℕ} : IsUnit <| W.dblZ P ^ n := (isUnit_dblZ_of_Y_ne' hP hQ hPz hx hy).pow n
erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, ←
dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]
