AlgebraicIntegralClosure.lean

theorem minpoly_coeff_mem_of_mem_extension
    {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
    (V : ValuationSubring K) [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (B : ValuationSubring Ω) [V.valuation.HasExtension B.valuation]
    (α : Ω) (hαB : α ∈ B) :
    ∀ i : ℕ, (minpoly K α).coeff i ∈ V

theorem isIntegral_of_mem_extension
    {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω]
    (V : ValuationSubring K) [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (B : ValuationSubring Ω) [V.valuation.HasExtension B.valuation]
    (α : Ω) (hαB : α ∈ B) : IsIntegral V α

theorem integralClosure_mem_or_inv_of_henselianRing
    {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L]
    (V : ValuationSubring K) [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (z : L) :
    z ∈ (integralClosure V L).toSubring ∨
      z⁻¹ ∈ (integralClosure V L).toSubring