ψ — Mathlib · SciLib

English

The bivariate n-division polynomials ψ_n are defined by applying a normEDS construction to W.ψ₂, W.Ψ₃, and W.preΨ₄ with parameter n.

Русский

Бивариантные многочлены ψ_n являются результатом применения нормированного конструктора normEDS к W.ψ₂, W.Ψ₃ и W.preΨ₄ с параметром n.

LaTeX

$$$W.\\\\psi(n) = normEDS(W.\\psi_2, C(W.\\Ψ_3), C(W.preΨ_4), n)$$$

Lean4

/-- The bivariate `n`-division polynomials `ψₙ`. -/
protected noncomputable def ψ (n : ℤ) : R[X][Y] :=
  normEDS W.ψ₂ (C W.Ψ₃) (C W.preΨ₄) n

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