ofJ1728_c₄

Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.ofJ1728_c₄

English

For the J=1728 model, the coefficient c4 equals −48: c4 = −48.

Русский

Для модели с j=1728 коэффициент c4 равен −48: c4 = −48.

LaTeX

$$$$ (ofJ1728 \; R).c_4 = -48 $$$$

Lean4

theorem ofJ1728_c₄ : (ofJ1728 R).c₄ = -48 := by
  rw [ofJ1728, c₄, b₂, b₄]
  norm_num1

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

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

Разделы

Аффилиация

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