English
Under NoZeroDivisors, and with P, Q satisfying equation relations and nonzero z-coordinates, negDblY(P)/dblZ(P)^3 equals the affine expression for Y-coordinate given by the affine slope and the Y-add formula.
Русский
При отсутствии нулей делителей и при выполнении условий для P, Q, включая неравный нуль z-координат, отношение negDblY(P) к dblZ(P)^3 равно аффинному выражению для Y-переменной, задаваемому наклонной прямой и правилу добавления.
LaTeX
$$$W'.\\mathrm{negDblY}(P) / W'.\\mathrm{dblZ}(P)^3 = W'.\\mathrm{toAffine}.\\mathrm{negAddY}\\left( P_x/P_z^2, Q_x/Q_z^2, P_y/P_z^3 \\right\\, (W'.\\mathrmtoAffine.slope( P_x/P_z^2, Q_x/Q_z^2, P_y/P_z^3, Q_y/Q_z^3))\\right)$$$
Lean4
theorem negDblY_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.negDblY P / W.dblZ P ^ 3 =
W.toAffine.negAddY (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)) :=
by
rw [negDblY, dblX, toAffine_slope_of_eq hP hQ hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]
