polynomialX — Mathlib

English

The homogeneous polynomial X-coordinate derivative component polynomialX is explicitly given by: W'.polynomialX = C(W'.a1)·Y·Z − (3·X^2 + 2·W'.a2·X·Z + W'.a4·Z^2).

Русский

Гомогенный производный по X многочлен polynomialX задаётся явной формулой: W'.polynomialX = C(W'.a1)·Y·Z − (3·X^2 + 2·W'.a2·X·Z + W'.a4·Z^2).

LaTeX

$$$W'.polynomialX = C\,W'.a_1 \\cdot Y \\cdot Z - \\bigl( C\\,3 \\cdot X^2 + C\\,(2\\cdot W'.a_2) \\cdot X \\cdot Z + C\\,W'.a_4 \\cdot Z^2 \\bigr)$$$

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 projective coordinates. -/
noncomputable def polynomialX : MvPolynomial (Fin 3) R :=
  pderiv x W'.polynomial

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