polynomialZ_eq — Mathlib

English

The Z-coordinate polynomial is given by a combination of X, Y, Z with the Weierstrass coefficients a1, a2, a3, a4, a6.

Русский

Z-координатный полином выражен через X, Y, Z и коэффициенты a1, a2, a3, a4, a6.

LaTeX

$$$ W'.polynomialZ = C W'.a_1 \\cdot X \\cdot Y + C(3 \\cdot W'.a_3) \\cdot Y \\cdot Z^{2} - \\left( C(2 \\cdot W'.a_2) X^{2} Z + C(4 \\cdot W'.a_4) X Z^{3} + C(6 \\cdot W'.a_6) Z^{5} \\right)$$$

Lean4

theorem polynomialZ_eq :
    W'.polynomialZ =
      C W'.a₁ * X * Y + C (3 * W'.a₃) * Y * Z ^ 2 -
        (C (2 * W'.a₂) * X ^ 2 * Z + C (4 * W'.a₄) * X * Z ^ 3 + C (6 * W'.a₆) * Z ^ 5) :=
  by
  rw [polynomialZ, polynomial]
  pderiv_simp
  ring1

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