English
Let W' be a projective Weierstrass curve over a ring. For two points P and Q given by triples P, Q : Fin 3 → R, with P z ≠ 0, Q z ≠ 0 and the cross-multiplication P x Q z = Q x P z, there is a cubic relation between the Y-coordinate of the sum and the coordinates of P and Q: (W'.addY P Q) (P z Q z)^3 = - (P y Q z - Q y P z)^3 (P z Q z)^2.
Русский
Пусть W' — проективная кривая Вейерштрасса над кольцом. Для точек P, Q ∈ Fin 3 → R с P z ≠ 0, Q z ≠ 0 и P x Q z = Q x P z существует кубическое соотношение между координатой y суммы и координатами P, Q: (W'.addY P Q)(P z Q z)^3 = - (P y Q z - Q y P z)^3 (P z Q z)^2.
LaTeX
$$$\big(W'.addY\,P\,Q\big) \cdot (P_z Q_z)^3 = -\big(P_y Q_z - Q_y P_z\big)^3 \cdot (P_z Q_z)^2$$$
Lean4
theorem addY_of_X_eq' [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) :
W'.addY P Q * (P z * Q z) ^ 3 = -(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 := by
linear_combination (norm := (rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx, addZ_of_X_eq hP hQ hPz hQz hx]; ring1))
-(P z * Q z) * negAddY_of_X_eq' hP hQ hx
