polynomialX_eq — Mathlib

English

The univariate polynomial X on the Weierstrass Jacobian satisfies a standard Weierstrass form: polynomialX equals a linear combination with a1, a2, a4, and the X, Y, Z coordinates.

Русский

Однородный полином X на Джейкобьяне Вейерштрасса удовлетворяет стандартной форме: polynomialX выражается как линейная комбинация с a1, a2, a4 и координатами X, Y, Z.

LaTeX

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

Lean4

theorem polynomialX_eq :
    W'.polynomialX = C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z ^ 2 + C W'.a₄ * Z ^ 4) :=
  by
  rw [polynomialX, polynomial]
  pderiv_simp
  ring1

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