ofJ0_j — Mathlib

English

Assuming j and j − 1728 are units, the Weierstrass curve of JNe0Or1728 is elliptic.

Русский

Пусть j и j − 1728 — единицы; тогда кривая Вейерштрасса WeierstrassCurve.ofJNe0Or1728 j является эллиптической.

LaTeX

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

Lean4

theorem ofJ0_j [Fact (IsUnit (3 : R))] : (ofJ0 R).j = 0 :=
  by
  rw [j, ofJ0_c₄]
  ring1
    -- TODO: change to `[IsUnit ...]` once https://github.com/leanprover-community/mathlib4/issues/17458 is merged

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