English
If there exist conditions with Y-ne, and with Zneq and Xne, then W.add P Q equals a scalar multiple of W.dblZ P times a 3-vector defined by affine coordinates and slope.
Русский
Если существуют условия Y-ne' и Z_ne не ноль, X_ne, то W.add P Q выражается как скалярное умножение на W.dblZ P некоторого вектора, заданного аффинными координатами и наклоном.
LaTeX
$$$ W.add P Q = W.dblZ P \\cdot \\llbracket \\text{..}\, , \\text{..}, 1 \\rrbracket $$$
Lean4
theorem add_of_Y_ne' [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.add P Q =
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)),
W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
(W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
1] :=
by
rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy,
dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]
