polynomialY — Mathlib

English

The Y-coordinate polynomial of W' is the partial derivative of the Weierstrass polynomial with respect to Y.

Русский

Y-координатный полином W' — это частная производная полинома W' по переменной Y.

LaTeX

$$$ W'.polynomialY = \\frac{\\partial}{\\partial Y} W'.polynomial $$$

Lean4

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

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