polynomialY_eq — Mathlib

English

The Y-coordinate polynomial is given explicitly by a linear combination involving Y and the Weierstrass coefficients a1 and a3, together with X and Z terms.

Русский

Y-полином выражается явным образом как линейная комбинация, включающая Y и коэффициенты a1, a3, а также X и Z-части.

LaTeX

$$$ W'.polynomialY = (C\\,2) \\cdot Y + C(W'.a_1) \\cdot X \\cdot Z + C(W'.a_3) \\cdot Z^3 $$$

Lean4

theorem polynomialY_eq : W'.polynomialY = C 2 * Y + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 3 :=
  by
  rw [polynomialY, polynomial]
  pderiv_simp
  ring1

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