ΨSq_two

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

English

The univariate ΨSq at two equals Ψ₂Sq: ΨSq(2) = Ψ₂Sq.

Русский

Значение ΨSq в 2 равно Ψ₂Sq: ΨSq(2) = Ψ₂Sq.

LaTeX

$$$W.\\PsiSq(2) = W.\\Psi_2S_q$$$

Lean4

@[simp]
theorem ΨSq_two : W.ΨSq 2 = W.Ψ₂Sq := by simp [ΨSq]

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

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

Разделы

Аффилиация

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