Φ_three

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Φ_three

← MathLib Explorer

English

The Φ-polynomial at index 3 equals X times Ψ₃^2 minus a product of preΨ₄ and Ψ₂Sq.

Русский

Φ_3 = X Ψ₃^2 − preΨ₄ Ψ₂Sq.

LaTeX

$$$W.\\Φ 3 = X \cdot W.\\Ψ_3^2 - W.preΨ_4 \cdot W.\\Ψ_2Sq$$$

Lean4

@[simp]
theorem Φ_three : W.Φ 3 = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq := by
  rw [show 3 = ((2 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_three, if_pos <| by decide, mul_one, preΨ'_four, preΨ'_two,
    mul_one, if_pos even_two]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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