ofJ — Mathlib

English

Assuming 2 is a unit, the Weierstrass curve with j=1728 is elliptic.

Русский

Предположим, что 2 является единицей; кривая Вейерштрасса с j=1728 является эллиптической.

LaTeX

$$$$ (ofJ1728 \; R).IsElliptic $$$$

Lean4

/-- For any element j of a field `F`, there exists an elliptic curve over `F`
with j-invariant equal to j (see `WeierstrassCurve.ofJ_j`).
Its coefficients are given explicitly (see `WeierstrassCurve.ofJ0`, `WeierstrassCurve.ofJ1728`
and `WeierstrassCurve.ofJNe0Or1728`). -/
def ofJ : WeierstrassCurve F :=
  if j = 0 then if (3 : F) = 0 then ofJ1728 F else ofJ0 F else if j = 1728 then ofJ1728 F else ofJNe0Or1728 j

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