ΨSq_four

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.ΨSq_four

English

The univariate ΨSq at four equals preΨ₄² times Ψ₂Sq: ΨSq(4) = preΨ₄² · Ψ₂Sq.

Русский

Значение ΨSq в 4 равно preΨ₄² умноженное на Ψ₂Sq: ΨSq(4) = preΨ₄² · Ψ₂Sq.

LaTeX

$$$W.\\PsiSq(4) = W.pre\\Psi_4^2 \cdot W.\\Psi_2S_q$$$

Lean4

@[simp]
theorem ΨSq_four : W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq := by simp [ΨSq, show ¬Odd (4 : ℤ) by decide]

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

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

Разделы

Аффилиация

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