ofJ1728_j — Mathlib

English

For j with unit conditions, the discriminant of the Weierstrass curve JNe0Or1728 j equals Δ = j^2 (j − 1728)^9.

Русский

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

LaTeX

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

Lean4

theorem ofJ1728_j [Fact (IsUnit (2 : R))] : (ofJ1728 R).j = 1728 :=
  by
  rw [j, Units.inv_mul_eq_iff_eq_mul, ofJ1728_c₄, coe_Δ', ofJ1728_Δ]
  norm_num1

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