eval_polynomial — Mathlib

English

The Weierstrass polynomial W' associated to a projective Weierstrass curve is the explicit symmetric polynomial in the coordinate functions X, Y, Z with the coefficients a1, a2, a3, a4, a6.

Русский

Полином Вейерштрасса W', связанный с кривой, задаётся явно через координаты X, Y, Z и коэффициенты a1, a2, a3, a4, a6.

LaTeX

$$W'.polynomial = Y^2 Z + C W'.a1 X Y Z + C W'.a3 Y Z^2 - (X^3 + C W'.a2 X^2 Z + C W'.a4 X Z^2 + C W'.a6 Z^3)$$

Lean4

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

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