eval_polynomial — Mathlib

English

The evaluation of the Jacobian polynomial at a point P is given by the explicit combination of the coordinates of P with the Weierstrass coefficients.

Русский

Значение полинома Жакобиана в точке P задаётся явным сочетанием координат P с коэффициентами Вейерштрасса.

LaTeX

$$eval P W'.polynomial = P_y^2 + a₁ P_x P_y P_z + a₃ P_y P_z^3 - (P_x^3 + a₂ P_x^2 P_z^2 + a₄ P_x P_z^4 + a₆ P_z^6)$$

Lean4

theorem eval_polynomial (P : Fin 3 → R) :
    eval P W'.polynomial =
      P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) :=
  by
  rw [polynomial]
  simp

Похожие утверждения