preΨ — Mathlib

English

Let W be a Weierstrass curve over a commutative ring. The univariate preΨ' at 3 equals Ψ₃: preΨ'(3) = Ψ₃.

Русский

Пусть W — кривая Вейерштрасса над коммутативной кольцевой структурой. Предварительный предикат preΨ'(3) равен Ψ₃: preΨ'(3) = Ψ₃.

LaTeX

$$$W.pre\\Psi'(3) = W.\\Psi_3$$$

Lean4

/-- The univariate polynomials `preΨₙ` for `n ∈ ℤ`, which are auxiliary to the bivariate polynomials
`Ψₙ` congruent to the bivariate `n`-division polynomials `ψₙ`. -/
noncomputable def preΨ (n : ℤ) : R[X] :=
  preNormEDS (W.Ψ₂Sq ^ 2) W.Ψ₃ W.preΨ₄ n

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