ofJNe0Or1728_Δ — Mathlib

English

For the Weierstrass model with parameter j (not equal to 0 or 1728), the discriminant Δ equals Δ = j^2 (j − 1728)^9.

Русский

Для кривой с параметром j (не равным 0 и 1728) дискриминант Δ равен Δ = j^2 (j − 1728)^9.

LaTeX

$$$$ (ofJNe0Or1728 \; j).\Delta = j^2 \cdot (j - 1728)^9 $$$$

Lean4

theorem ofJNe0Or1728_Δ : (ofJNe0Or1728 j).Δ = j ^ 2 * (j - 1728) ^ 9 :=
  by
  simp only [ofJNe0Or1728, Δ, b₂, b₄, b₆, b₈]
  ring1

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