ofJNe0Or1728_j

Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.ofJNe0Or1728_j

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem ofJNe0Or1728_j (j : R) [Fact (IsUnit j)] [Fact (IsUnit (j - 1728))] : (ofJNe0Or1728 j).j = j :=
  by
  rw [WeierstrassCurve.j, Units.inv_mul_eq_iff_eq_mul, ofJNe0Or1728_c₄, coe_Δ', ofJNe0Or1728_Δ]
  ring1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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