ofJ1728_Δ

Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.ofJ1728_Δ

English

For the J=1728 model, the discriminant Δ equals −64: Δ = −64.

Русский

Для модели с j=1728 дискриминант Δ равен −64.

LaTeX

$$$$ (ofJ1728 \; R).\Delta = -64 $$$$

Lean4

theorem ofJ1728_Δ : (ofJ1728 R).Δ = -64 := by
  rw [ofJ1728, Δ, b₂, b₄, b₆, b₈]
  norm_num1

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

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

Разделы

Аффилиация

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