English
The univariate auxiliary polynomials preΨ'_n are defined as the preNormEDS' combination of Ψ₂Sq^2, Ψ₃, and preΨ₄ in the Weierstrass curve.
Русский
Вводятся вспомогательные одночлены preΨ'_n как композиция preNormEDS' из Ψ₂Sq^2, Ψ₃ и preΨ₄ для кривой Вейерштрасса.
LaTeX
$$$$\text{preΨ}'(n) = \text{preNormEDS}'(W.\Psi_2Sq^2, W.\Psi_3, W.preΨ_4, n).$$$$
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