ofJNe0Or1728_c₄ — Mathlib

English

For the Weierstrass model with parameter j (not equal to 0 or 1728), the c4 coefficient is c4 = j (j − 1728)^3.

Русский

Для кривой Вейерштрасса с параметром j (не равным 0 и не равным 1728) коэффициент c4 равен c4 = j (j − 1728)^3.

LaTeX

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

Lean4

theorem ofJNe0Or1728_c₄ : (ofJNe0Or1728 j).c₄ = j * (j - 1728) ^ 3 :=
  by
  simp only [ofJNe0Or1728, c₄, b₂, b₄]
  ring1

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