instIsEllipticOfJ1728OfFactIsUnitOfNat

English

For j satisfying unit conditions, the j-invariant of the Weierstrass curve of JNe0Or1728 j equals j.

Русский

Для j, удовлетворяющего условиям единичности, инварианта j кривой WeierstrassCurve.ofJNe0Or1728 j равен j.

LaTeX

$$$$ (ofJNe0Or1728 j).j = j $$$$

Lean4

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

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