FinitelyGeneratedValuationDetection.lean

theorem exists_finiteType_int_model_le_valuationSubring
    (K : Type u) [Field K] (hfg : Field.FG K)
    (V : ValuationSubring K) (y : K) (hy : y ∈ V) :
    ∃ A : Subalgebra ℤ K, Algebra.FiniteType ℤ A ∧ IsFractionRing A K ∧
      A.toSubring ≤ V.toSubring ∧ y ∈ A

theorem exists_discreteValuationSubring_inv_nonunit_of_not_integral
    (K : Type u) [Field K] (hfg : Field.FG K)
    (x : K) (hx : ¬ IsIntegral ℤ x) :
    ∃ W : ValuationSubring K, IsDiscreteValuationRing W ∧ x⁻¹ ∈ W.nonunits

theorem exists_DVF_detect_nonconstant
    (K : Type u) [Field K] (hfg : Field.FG K)
    (x : K) (hx : x ∉ algebraicClosure (⊥ : Subfield K) K) :
    ∃ D : ValuationTheory.DiscreteValuationField.DVF.{u, 0} K,
      D.valuation x ≠ 1