instIsEllipticOfJNe0Or1728OfFactIsUnitHSubOfNat

English

For j in JNe0Or1728, the c4 coefficient is c4 = j (j − 1728)^3.

Русский

Для j в JNe0Or1728 коэффициент c4 равен c4 = j (j − 1728)^3.

LaTeX

$$$$ (ofJNe0Or1728 j).c_4 = j \cdot (j - 1728)^3 $$$$

Lean4

/-- When j and j - 1728 are both units,
`Y² + (j - 1728)XY = X³ - 36(j - 1728)³X - (j - 1728)⁵` is an elliptic curve.
It is of j-invariant j (see `WeierstrassCurve.ofJNe0Or1728_j`). -/
instance (j : R) [h1 : Fact (IsUnit j)] [h2 : Fact (IsUnit (j - 1728))] : (ofJNe0Or1728 j).IsElliptic :=
  by
  rw [isElliptic_iff, ofJNe0Or1728_Δ]
  exact
    (h1.out.pow 2).mul
      (h2.out.pow 9)
        -- TODO: change to `[IsUnit ...]` once https://github.com/leanprover-community/mathlib4/issues/17458 is merged

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