English
Assume that P and Q lie on the Weierstrass curve with P z ≠ 0, Q z ≠ 0 and the Y-relations make certain equalities hold; then W'.dblX P equals zero: the X-coordinate vanishes under those Y-equality hypotheses.
Русский
Пусть P и Q лежат на кривой Вейерштрасса и P_z ≠ 0, Q_z ≠ 0, а условия по Y приводят к равенствам; тогда W'.dblX P = 0.
LaTeX
$$$ {P Q: Fin 3 → F} (hP: W'.Equation P) (hPz: P z ≠ 0) (hQz: Q z ≠ 0) (hx: P x Q z = Q x P z) (hy: P y Q z = Q y P z) (hy': P y Q z = W'.negY Q P z) : W'.dblX P = 0 $$$
Lean4
theorem dblX_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) (hy : P y * Q z ≠ W.negY Q * P z) :
W.dblX P / W.dblZ P =
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)) :=
by
rw [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hP hQ hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
toAffine_addX_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]
