polynomialX — Mathlib

English

The X-coordinate polynomial of the Weierstrass Jacobian, polynomialX, is the partial derivative of the Weierstrass polynomial W' with respect to X.

Русский

X-полином Якобиана — частная производная полинома Вейерштрасса по переменной X.

LaTeX

$$$\\text{polynomialX} = \\frac{\\partial}{\\partial X} W'.polynomial$$$

Lean4

/-- The partial derivative `W_X(X, Y, Z)` with respect to `X` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in Jacobian coordinates. -/
noncomputable def polynomialX : MvPolynomial (Fin 3) R :=
  pderiv x W'.polynomial

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