C_Ψ₂Sq — Mathlib

English

The polynomial identity relating C Ψ₂Sq to ψ₂ and the affine coordinate polynomial holds on a Weierstrass curve.

Русский

Полиномиальное тождество между C Ψ₂Sq и ψ₂ с аффинным координатным полиномом выполняется для кривой Вейерштрасса.

LaTeX

$$$$C \Psi_2^2 = \psi_2^2 - 4 \cdot \text{AffinePolynomial}.$$$$

Lean4

theorem C_Ψ₂Sq : C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial :=
  by
  rw [Ψ₂Sq, ψ₂, b₂, b₄, b₆, Affine.polynomialY, Affine.polynomial]
  C_simp
  ring1

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