theorem GenusOneCurve.jInvariant_in_k {k : Type u} [Field k] (C : GenusOneCurve k) (O : C.PointOverAlgClosure) : (C.ellipticCurveAtBasePoint O).jInvariant ∈ Set.range ⇑(algebraMap k (AlgebraicClosure k))