ψ_four — Mathlib

English

For a Weierstrass curve W over a commutative ring, the polynomial ψ at 4 factors as ψ4 = (preΨ4)·ψ2, i.e. ψ4 = C(preΨ4) · ψ2.

Русский

Для кривой Вейерштрасса W над коммутативным кольцом полином ψ при 4 факторизуется как ψ4 = (preΨ4)·ψ2, то есть ψ4 = C(preΨ4)·ψ2.

LaTeX

$$$\\psi_4 = C(\\text{pre}\\Psi_4) \\cdot \\psi_2$$$

Lean4

@[simp]
theorem ψ_four : W.ψ 4 = C W.preΨ₄ * W.ψ₂ :=
  normEDS_four ..

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