instIsEllipticOfJ0OfFactIsUnitOfNat

English

If j and j − 1728 are units in a ring, then the Weierstrass curve defined by JNe0Or1728 j is elliptic.

Русский

Если j и j − 1728 являются единицами в кольце, то кривая Вейершстраса, заданная через JNe0Or1728 j, является эллиптической.

LaTeX

$$$$ (ofJNe0Or1728 j).IsElliptic $$$$

Lean4

/-- When 3 is a unit, `Y² + Y = X³` is an elliptic curve.
It is of j-invariant 0 (see `WeierstrassCurve.ofJ0_j`). -/
instance [hu : Fact (IsUnit (3 : R))] : (ofJ0 R).IsElliptic :=
  by
  rw [isElliptic_iff, ofJ0_Δ]
  convert (hu.out.pow 3).neg
  norm_num1
    -- TODO: change to `[IsUnit ...]` once https://github.com/leanprover-community/mathlib4/issues/17458 is merged

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