English
Under the Weierstrass projective model, with P,Q on the curve and hy', hy, hy relations, the dblY P satisfies a cubic relation with P coordinates and P z.
Русский
В модельной проективной кривой Weierstrass, если P,Q на кривой и соблюдены hy', hy, hy', dblY P удовлетворяет кубическому соотношению по координатам P и P z.
LaTeX
$$$ {P Q: Fin 3→F} (hP: W'.Equation P) (hQ: W'.Equation Q) (hPz: P z ≠ 0) (hQz: Q z ≠ 0) (hy: P y Q z = Q y P z) (hy': P y Q z = W'.negY Q P z) : W'.dblY P ^? = \cdots$$$
Lean4
theorem dblY_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'.dblY P * P z ^ 2 = eval P W'.polynomialX ^ 3 := by
linear_combination (norm :=
(rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']; ring1))
-negDblY_of_Y_eq' hP hQz hx hy hy'
