English
There is an instance that states the ellipticity of the model for a generic j, given IsElliptic conditions are satisfied.
Русский
Существует экземпляр, который устанавливает эллиптичность модели для произвольного j при выполнении условий эллиптичности.
LaTeX
$$$$ (ofJ j).IsElliptic $$$$
Lean4
instance : (ofJ j).IsElliptic := 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))
rw [h0, ofJ_0_of_three_eq_zero h3]
infer_instance
· have := Fact.mk (Ne.isUnit h3)
rw [h0, ofJ_0_of_three_ne_zero h3]
infer_instance
· by_cases h1728 : j = 1728
· have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
have := Fact.mk h2.isUnit
rw [h1728, ofJ_1728_of_two_ne_zero h2]
infer_instance
· have := Fact.mk (Ne.isUnit h0)
have := Fact.mk (sub_ne_zero.2 h1728).isUnit
rw [ofJ_ne_0_ne_1728 j h0 h1728]
infer_instance
