English
Assume R has NoZeroDivisors, and P, Q are two points on the Weierstrass projective curve with Q z ≠ 0 and the standard cross-relations hx, hy, hy'. If X- and Y-conditions hold and the Y-relations avoid degeneracy, then the Z-coordinate of 2P is nonzero: W'.dblZ P ≠ 0.
Русский
Пусть R не имеет нулей делителей, и P, Q — две точки на проективной кривой Вейерштрасса; если Q z ≠ 0 и выполняются предписанные перекрёстные соотношения hx, hy, hy', избегая вырождения Y, то Z-координата удвоенной точки не равна нулю: W'.dblZ P ≠ 0.
LaTeX
$$$ [NoZeroDivisors\ R] \; P,Q: \mathrm{Fin}(3)→R,\; W'.Equation P,\; W'.Equation Q,\; P z ≠ 0,\; Q z ≠ 0,\; hx: P_x Q_z = Q_x P_z,\; hy: P_y Q_z ≠ Q_y P_z,\; \Rightarrow W'.\mathrm{dblZ} P ≠ 0$$$
Lean4
theorem dblZ_ne_zero_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (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 ≠ Q y * P z) : W'.dblZ P ≠ 0 :=
mul_ne_zero hPz <| pow_ne_zero 3 <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne hP hQ hPz hQz hx hy
