ψ_odd

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.ψ_odd

English

The odd-indexed division polynomials satisfy ψ(2m+1) = ψ(m+2)·ψ(m)^3 − ψ(m−1)·ψ(m+1)^3.

Русский

Для нечётных индексов выполняется тождество: ψ(2m+1) = ψ(m+2)·ψ(m)^3 − ψ(m−1)·ψ(m+1)^3.

LaTeX

$$$\\psi(2m+1) = \\psi(m+2) \\psi(m)^3 - \\psi(m-1) \\psi(m+1)^3$$$

Lean4

theorem ψ_odd (m : ℤ) : W.ψ (2 * m + 1) = W.ψ (m + 2) * W.ψ m ^ 3 - W.ψ (m - 1) * W.ψ (m + 1) ^ 3 :=
  normEDS_odd ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru