English
Let P, Q be affine coordinates on a Weierstrass Jacobian with P_z ≠ 0 and Q_z ≠ 0. Then the relation P_y Q_z^3 = W.negY(Q) P_z^3 is equivalent to P_y / P_z^3 = W.toAffine.negY (Q_x / Q_z^2) (Q_y / Q_z^3).
Русский
Пусть P, Q — аффинные координаты на канонической кривой Вейершстраса в Якобиане; если P_z ≠ 0 и Q_z ≠ 0, то соотношение P_y Q_z^3 = W.negY(Q) P_z^3 эквивалентно P_y / P_z^3 = W.toAffine.negY (Q_x / Q_z^2) (Q_y / Q_z^3).
LaTeX
$$$\forall P,Q: (P_2 \neq 0) \wedge (Q_2 \neq 0) \Rightarrow P_1 Q_2^3 = W.negY(Q) P_2^3 \iff P_1 / P_2^3 = W.toAffine.negY (Q_0 / Q_2^2) (Q_1 / Q_2^3)$$$
Lean4
theorem Y_eq_iff' {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
P y * Q z ^ 3 = W.negY Q * P z ^ 3 ↔ P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3) :=
negY_of_Z_ne_zero hQz ▸ (div_eq_div_iff (pow_ne_zero 3 hPz) (pow_ne_zero 3 hQz)).symm
