IsIntegral_adjoin_of_forall_mem_toValuationSubring.lean

theorem isIntegral_of_mem_adjoin_inv {A F : Type*} [CommRing A] [Field F] [Algebra A F]
    {z : F} (hz0 : z ≠ 0) (hmem : z ∈ Algebra.adjoin A ({z⁻¹} : Set F)) : IsIntegral A z

theorem isIntegral_of_forall_valuationSubring {F : Type*} [Field F] (A : Subring F) (z : F)
    (h : ∀ V : ValuationSubring F, A ≤ V.toSubring → z ∈ V) : IsIntegral A z

theorem _root_.AlgebraicCurve.isIntegral_adjoin_of_forall_mem_toValuationSubring
    {K F : Type*} [Field K] [Field F] [Algebra K F] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F]
    (t z : F)
    (h : ∀ v : AlgebraicCurve.Place K F, t ∈ v.toValuationSubring → z ∈ v.toValuationSubring) :
    IsIntegral (Algebra.adjoin K ({t} : Set F)) z