English
If P satisfies the Weierstrass Equation on W, then the value of W.dblX P equals a certain rational expression in the coordinates of P divided by P z, i.e., W.dblX P = [large polynomial]/P z.
Русский
Если P удовлетворяет уравнению Вейерштрасса на W, то значение W.dblX P равно заданному рациональному выражению в координатах P, делённому на P z: W.dblX P = [многочлен]/P z.
LaTeX
$$$ {P: \mathrm{Fin}(3)→F} \; (hP: W'.Equation P) (hPz: P z ≠ 0) : W'.dblX P = \frac{(eval P W'.polynomialX^2 - \cdots)}{P z}$$$
Lean4
theorem dblX_eq {P : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) :
W.dblX P =
((eval P W.polynomialX ^ 2 - W.a₁ * eval P W.polynomialX * P z * (P y - W.negY P) -
W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
2 * P x * P z * (P y - W.negY P) ^ 2) *
(P y - W.negY P)) /
P z :=
by rw [← dblX_eq' hP, mul_div_cancel_right₀ _ hPz]
