ValuationSubring_exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic.lean

lemma exists_ne_map_eq_of_sum_eq_zero {R : Type*} [CommRing R]
    {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
    {ι : Type*} (s : Finset ι) (t : ι → R) (hs : s.Nonempty) (ht : ∀ i ∈ s, v (t i) ≠ 0)
    (hsum : ∑ i ∈ s, t i = 0) : ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ v (t i) = v (t j)

lemma exists_lt_valuation_eq {E F : Type*} [Field E] [Field F] [Algebra E F]
    (O : ValuationSubring F) {g : F} (hg : g ≠ 0) {p : Polynomial E} (hp : p ≠ 0)
    (hpg : Polynomial.aeval g p = 0) :
    ∃ i j : ℕ, i < j ∧ p.coeff i ≠ 0 ∧ p.coeff j ≠ 0 ∧
      O.valuation (algebraMap E F (p.coeff i) * g ^ i) =
        O.valuation (algebraMap E F (p.coeff j) * g ^ j)

theorem _root_.ValuationSubring.exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic
    {E F : Type*} [Field E] [Field F] [Algebra E F] [Algebra.IsAlgebraic E F]
    (O : ValuationSubring F) {g : F} (hg : g ≠ 0) :
    ∃ n : ℕ, 0 < n ∧ ∃ c : E, c ≠ 0 ∧ O.valuation (g ^ n) = O.valuation (algebraMap E F c)