English
If P and Q are on W with nonzero Z-components and P z ≠ 0, Q z ≠ 0, then the affine X-coordinate of 2P can be computed using the slope of the line through P and Q, yielding W.dblX P / W.dblZ P = ... (affine formula).
Русский
Если P и Q лежат на W и их Z-координаты ненулевые, то аффинное X-координата точки 2P может быть выражена через наклон линии через P и Q: W.dblX P / W.dblZ P = ... (аффинная формула).
LaTeX
$$$ [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 ≠ Q y P z) : \frac{W'.dblX P}{W'.dblZ P} = \text{AffineX}(P,Q,hx,hy) $$$
Lean4
theorem dblX_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (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 :=
by
apply eq_zero_of_ne_zero_of_mul_right_eq_zero hPz
rw [dblX_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']
ring1
