ofJ0_Δ

Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

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

English

Let R be a commutative ring and W a Weierstrass curve over R. In the J=0 model, the discriminant Δ equals −27: Δ = −27.

Русский

Пусть R — коммутативное кольцо, W — кривая Вейершстра над R. В модели с j=0 дискриминант Δ равен −27.

LaTeX

$$$$ (ofJ0 \; R).\Delta = -27 $$$$

Lean4

theorem ofJ0_Δ : (ofJ0 R).Δ = -27 := by
  rw [ofJ0, Δ, b₂, b₄, b₆, b₈]
  norm_num1

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

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

Разделы

Аффилиация

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