English
Evaluating the Weierstrass polynomial W' on a point P yields the explicit combination of P’s coordinates with the curve coefficients.
Русский
Подстановка точек P в полином W' для кривой Вейерштрасса даёт явное сочетание координат P с коэффициентами кривой.
LaTeX
$$eval P W'.polynomial = P y^2 P z + W'.a1 P x P y P z + W'.a3 P y P z^2 - (P x^3 + W'.a2 P x^2 P z + W'.a4 P x P z^2 + W'.a6 P z^3)$$
Lean4
/-- The polynomial `W(X, Y, Z) := Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³)` associated to a
Weierstrass curve `W` over a ring `R` in projective coordinates.
This is represented as a term of type `MvPolynomial (Fin 3) R`, where `X`, `Y`, and `Z`
represent `X`, `Y`, and `Z` respectively. -/
noncomputable def polynomial : MvPolynomial (Fin 3) R :=
Y ^ 2 * Z + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 2 -
(X ^ 3 + C W'.a₂ * X ^ 2 * Z + C W'.a₄ * X * Z ^ 2 + C W'.a₆ * Z ^ 3)
