c_relation — Mathlib

English

The discriminant Δ of a Weierstrass curve satisfies the classical relation 1728 Δ equals c4^3 − c6^2.

Русский

Дискриминант кривой Вейерштрасса удовлетворяет классическому равенству 1728 Δ = c4^3 − c6^2.

LaTeX

$$$$ 1728 \cdot W.\Delta = W.c_4^3 - W.c_6^2 $$$$

Lean4

theorem c_relation : 1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2 :=
  by
  simp only [b₂, b₄, b₆, b₈, c₄, c₆, Δ]
  ring1

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