English
There is an ellipticity instance for the J=1728 model, given 2 is a unit.
Русский
Существует экземпляр эллиптичности для модели j=1728 при условии, что 2 является единицей.
LaTeX
$$$$ (ofJ1728 j).IsElliptic $$$$
Lean4
theorem ofJ_j : (ofJ j).j = j := by
by_cases h0 : j = 0
· by_cases h3 : (3 : F) = 0
· have := Fact.mk (isUnit_of_mul_eq_one (2 : F) 2 (by linear_combination h3))
simp_rw [h0, ofJ_0_of_three_eq_zero h3, ofJ1728_j]
linear_combination 576 * h3
· have := Fact.mk (Ne.isUnit h3)
simp_rw [h0, ofJ_0_of_three_ne_zero h3, ofJ0_j]
· by_cases h1728 : j = 1728
· have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
have := Fact.mk h2.isUnit
simp_rw [h1728, ofJ_1728_of_two_ne_zero h2, ofJ1728_j]
· have := Fact.mk (Ne.isUnit h0)
have := Fact.mk (sub_ne_zero.2 h1728).isUnit
simp_rw [ofJ_ne_0_ne_1728 j h0 h1728, ofJNe0Or1728_j]
