j_of_isShortNF — Mathlib

English

Let W be a Weierstrass curve in short normal form over a field, then its j-invariant is given by j(W) = 6912 a4^3 / (4 a4^3 + 27 a6^2).

Русский

Пусть W — кривая Вейерштрасса в краткой нормальной форме над полем. Тогда её j-инварианта равна j(W) = 6912 a4^3 / (4 a4^3 + 27 a6^2).

LaTeX

$$$ j(W) = \dfrac{6912\, W.a_4^3}{4\, W.a_4^3 + 27\, W.a_6^2} $$$

Lean4

theorem j_of_isShortNF : W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) :=
  by
  have h := W.Δ'.ne_zero
  rw [coe_Δ', Δ_of_isShortNF] at h
  rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ', c₄_of_isShortNF, Δ_of_isShortNF,
    div_eq_div_iff h (right_ne_zero_of_mul h)]
  ring1

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