Ψ — Mathlib · SciLib

English

The bivariate polynomials Ψ_n associated to a Weierstrass curve are defined by combining the n-division structure with a factor that depends on evenness of n.

Русский

Связанные с кривой Вейерштрасса бивариатные многочлены Ψ_n задаются как комбинация n-делений и множителя, зависящего от того, чётно ли n.

LaTeX

$${R : Type r} → [CommRing R] → WeierstrassCurve R → Int → Polynomial (Polynomial R)$$

Lean4

/-- The bivariate polynomials `Ψₙ` congruent to the `n`-division polynomials `ψₙ`. -/
protected noncomputable def Ψ (n : ℤ) : R[X][Y] :=
  C (W.preΨ n) * if Even n then W.ψ₂ else 1

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