ExponentialValuations.lean

structure ExponentialValuation (K : Type*) [Field K] where
  /-- The value map into `ℝ ∪ {∞}`. -/
  toFun : K → WithTop ℝ
  /-- Exactly zero has value `∞`. -/
  eq_top_iff : ∀ x, toFun x = ⊤ ↔ x = 0
  /-- Multiplication becomes addition of values. -/
  map_mul : ∀ x y, toFun (x * y) = toFun x + toFun y
  /-- The nonarchimedean inequality in additive form. -/
  add_le_min : ∀ x y, min (toFun x) (toFun y) ≤ toFun (x + y)

instance exponentialValuationCoeFun {K : Type*} [Field K] :
    CoeFun (ExponentialValuation K) (fun _ => K → WithTop ℝ) where
  coe v := v.toFun

def TrivialExponentialValuation {K : Type*} [Field K]
    (v : ExponentialValuation K) : Prop

def EquivalentExponentialValuations {K : Type*} [Field K]
    (v w : ExponentialValuation K) : Prop

def AssociatedAbsoluteValue {K : Type*} [Field K]
    (v : ExponentialValuation K) (q : ℝ) (abv : AbsoluteValue K ℝ) : Prop

def exponentialValuationRing {K : Type*} [Field K]
    (v : ExponentialValuation K) : Set K

theorem exponentialValuation_ne_top_of_ne_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : K} (hx : x ≠ 0) :
    v x ≠ ⊤

theorem exponentialValuation_exists_real_of_ne_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : K} (hx : x ≠ 0) :
    ∃ r : ℝ, v x = (r : WithTop ℝ)

theorem exponentialValuation_one {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    v (1 : K) = 0

theorem exponentialValuation_neg_one {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    v (-1 : K) = 0

theorem exponentialValuation_neg {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : K) :
    v (-x) = v x

theorem exponentialValuation_ne_zero_of_value_eq_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : K} (hx : v x = 0) :
    x ≠ 0

theorem exponentialValuation_inv_of_value_eq_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : K} (hx : v x = 0) :
    v x⁻¹ = 0

theorem exponentialValuation_inv_value {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : K} (hx : x ≠ 0) {r : ℝ}
    (hval : v x = (r : WithTop ℝ)) :
    v x⁻¹ = ((-r : ℝ) : WithTop ℝ)

def exponentialValuationSubring {K : Type*} [Field K]
    (v : ExponentialValuation K) : Subring K where
  carrier := exponentialValuationRing v
  zero_mem' := by
    change (0 : WithTop ℝ) ≤ v (0 : K)
    rw [(v.eq_top_iff 0).mpr rfl]
    simp
  one_mem' := by
    change (0 : WithTop ℝ) ≤ v (1 : K)
    simp
  add_mem' := by
    intro x y hx hy
    change (0 : WithTop ℝ) ≤ v (x + y)
    exact (le_min hx hy).trans (v.add_le_min x y)
  neg_mem' := by
    intro x hx
    change (0 : WithTop ℝ) ≤ v x at hx
    change (0 : WithTop ℝ) ≤ v (-x)
    simpa using hx
  mul_mem' := by
    intro x y hx hy
    change (0 : WithTop ℝ) ≤ v (x * y)
    rw [v.map_mul]
    exact add_nonneg hx hy

theorem mem_exponentialValuationSubring_iff {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : K) :
    x ∈ exponentialValuationSubring v ↔ (0 : WithTop ℝ) ≤ v x

theorem exponentialValuationRing_mem_or_inv_mem {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : K) :
    x ∈ exponentialValuationRing v ∨ x⁻¹ ∈ exponentialValuationRing v

theorem exponentialValuationSubring_mem_or_inv_mem {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : K) :
    x ∈ exponentialValuationSubring v ∨
      x⁻¹ ∈ exponentialValuationSubring v

def exponentialValuationSubringAsValuationSubring
    {K : Type*} [Field K] (v : ExponentialValuation K) :
    ValuationSubring K

theorem mem_exponentialValuationSubringAsValuationSubring_iff
    {K : Type*} [Field K] (v : ExponentialValuation K) (x : K) :
    x ∈ exponentialValuationSubringAsValuationSubring v ↔
      (0 : WithTop ℝ) ≤ v x

def exponentialUnitSet {K : Type*} [Field K]
    (v : ExponentialValuation K) : Set K

def exponentialMaxIdealSet {K : Type*} [Field K]
    (v : ExponentialValuation K) : Set K

theorem equivalentExponentialValuations_value_nonneg_iff
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) (x : K) :
    (0 : WithTop ℝ) ≤ v x ↔ (0 : WithTop ℝ) ≤ w x

theorem equivalentExponentialValuations_value_eq_zero_iff
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) (x : K) :
    v x = 0 ↔ w x = 0

theorem equivalentExponentialValuations_value_pos_iff
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) (x : K) :
    (0 : WithTop ℝ) < v x ↔ (0 : WithTop ℝ) < w x

theorem equivalentExponentialValuations_ring_eq
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) :
    exponentialValuationRing v = exponentialValuationRing w

theorem equivalentExponentialValuations_subring_eq
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) :
    exponentialValuationSubring v = exponentialValuationSubring w

theorem equivalentExponentialValuations_valuationSubring_eq
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) :
    exponentialValuationSubringAsValuationSubring v =
      exponentialValuationSubringAsValuationSubring w

theorem equivalentExponentialValuations_unitSet_eq
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) :
    exponentialUnitSet v = exponentialUnitSet w

theorem equivalentExponentialValuations_maxIdealSet_eq
    {K : Type*} [Field K] {v w : ExponentialValuation K}
    (hequiv : EquivalentExponentialValuations v w) :
    exponentialMaxIdealSet v = exponentialMaxIdealSet w

theorem associatedAbsoluteValue_le_one_iff
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv) {x : K} (hx : x ≠ 0) :
    abv x ≤ 1 ↔ (0 : WithTop ℝ) ≤ v x

theorem associatedAbsoluteValue_lt_one_iff
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv) {x : K} (hx : x ≠ 0) :
    abv x < 1 ↔ (0 : WithTop ℝ) < v x

theorem associatedAbsoluteValue_eq_one_iff
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv) {x : K} (hx : x ≠ 0) :
    abv x = 1 ↔ v x = 0

theorem associatedAbsoluteValue_ring_eq_closed_unit_ball
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv) :
    exponentialValuationRing v = {x : K | abv x ≤ 1}

theorem associatedAbsoluteValue_unitSet_eq_unit_sphere
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv) :
    exponentialUnitSet v = {x : K | abv x = 1}

theorem associatedAbsoluteValue_maxIdealSet_eq_open_unit_ball
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv) :
    exponentialMaxIdealSet v = {x : K | abv x < 1}

theorem exponentialUnitSet_subset_ring {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    exponentialUnitSet v ⊆ exponentialValuationRing v

theorem exponentialMaxIdealSet_subset_ring {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    exponentialMaxIdealSet v ⊆ exponentialValuationRing v

def exponentialMaxIdeal {K : Type*} [Field K]
    (v : ExponentialValuation K) : Ideal (exponentialValuationSubring v) where
  carrier := {x | (0 : WithTop ℝ) < v (x : K)}
  zero_mem' := by
    change (0 : WithTop ℝ) < v (0 : K)
    rw [(v.eq_top_iff 0).mpr rfl]
    simp
  add_mem' := by
    intro x y hx hy
    change (0 : WithTop ℝ) < v ((x + y : exponentialValuationSubring v) : K)
    have hmin : (0 : WithTop ℝ) < min (v (x : K)) (v (y : K)) :=
      lt_min hx hy
    exact lt_of_lt_of_le hmin (by simpa using v.add_le_min (x : K) (y : K))
  smul_mem' := by
    intro a x hx
    change (0 : WithTop ℝ) < v ((a : K) * (x : K))
    have ha : (0 : WithTop ℝ) ≤ v (a : K) := a.property
    rw [v.map_mul]
    have hx_le : v (x : K) ≤ v (a : K) + v (x : K) := by
      simpa [zero_add] using
        (add_le_add ha (le_rfl : v (x : K) ≤ v (x : K)))
    exact lt_of_lt_of_le hx hx_le

theorem mem_exponentialMaxIdeal_iff {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : exponentialValuationSubring v) :
    x ∈ exponentialMaxIdeal v ↔ (0 : WithTop ℝ) < v (x : K)

theorem one_not_mem_exponentialMaxIdeal {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    (1 : exponentialValuationSubring v) ∉ exponentialMaxIdeal v

theorem not_mem_exponentialMaxIdeal_iff_value_eq_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : exponentialValuationSubring v) :
    x ∉ exponentialMaxIdeal v ↔ v (x : K) = 0

theorem isUnit_of_exponentialValuation_eq_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : exponentialValuationSubring v}
    (hx : v (x : K) = 0) :
    IsUnit x

theorem exponentialValuation_eq_zero_of_isUnit {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : exponentialValuationSubring v}
    (hx : IsUnit x) :
    v (x : K) = 0

theorem isUnit_of_not_mem_exponentialMaxIdeal {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : exponentialValuationSubring v}
    (hx : x ∉ exponentialMaxIdeal v) :
    IsUnit x

theorem not_mem_exponentialMaxIdeal_of_isUnit {K : Type*} [Field K]
    (v : ExponentialValuation K) {x : exponentialValuationSubring v}
    (hx : IsUnit x) :
    x ∉ exponentialMaxIdeal v

theorem isUnit_iff_not_mem_exponentialMaxIdeal {K : Type*} [Field K]
    (v : ExponentialValuation K) (x : exponentialValuationSubring v) :
    IsUnit x ↔ x ∉ exponentialMaxIdeal v

theorem associatedAbsoluteValue_isUnit_iff_eq_one
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {q : ℝ} {abv : AbsoluteValue K ℝ}
    (hassoc : AssociatedAbsoluteValue v q abv)
    (x : exponentialValuationSubring v) :
    IsUnit x ↔ abv (x : K) = 1

theorem exponentialMaxIdeal_isMaximal {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    (exponentialMaxIdeal v).IsMaximal

instance exponentialValuationSubringIsLocalRing {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    IsLocalRing (exponentialValuationSubring v)

theorem exponentialMaxIdeal_eq_maximalIdeal {K : Type*} [Field K]
    (v : ExponentialValuation K) :
    exponentialMaxIdeal v =
      IsLocalRing.maximalIdeal (exponentialValuationSubring v)

def DiscreteExponentialValuation {K : Type*} [Field K]
    (v : ExponentialValuation K) : Prop

def NormalizedExponentialValuation {K : Type*} [Field K]
    (v : ExponentialValuation K) : Prop

def PrimeElementFor {K : Type*} [Field K]
    (v : ExponentialValuation K) (π : K) : Prop

theorem primeElementFor_of_value_eq_one {K : Type*} [Field K]
    (v : ExponentialValuation K) {π : K}
    (hπ : v π = (1 : WithTop ℝ)) :
    PrimeElementFor v π

theorem normalizedExponentialValuation_exists_primeElement
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) :
    ∃ π : K, PrimeElementFor v π

def primeElementInValuationSubring {K : Type*} [Field K]
    (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) :
    exponentialValuationSubring v

theorem primeElement_mem_exponentialMaxIdeal
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) :
    primeElementInValuationSubring v hπ ∈ exponentialMaxIdeal v

theorem primeElement_mem_maximalIdeal
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) :
    primeElementInValuationSubring v hπ ∈
      IsLocalRing.maximalIdeal (exponentialValuationSubring v)

theorem primeElementInValuationSubring_ne_zero
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) :
    primeElementInValuationSubring v hπ ≠ 0

theorem primeElementInValuationSubring_not_isUnit
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) :
    ¬ IsUnit (primeElementInValuationSubring v hπ)

theorem primeElementFor_inv_value {K : Type*} [Field K]
    (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) :
    v π⁻¹ = ((-1 : ℝ) : WithTop ℝ)

theorem primeElementFor_pow_value {K : Type*} [Field K]
    (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    v (π ^ n) = ((n : ℝ) : WithTop ℝ)

theorem primeElementFor_pow_ne_zero {K : Type*} [Field K]
    (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    π ^ n ≠ 0

theorem primeElementFor_zpow_value {K : Type*} [Field K]
    (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) (m : ℤ) :
    v (π ^ m) = ((m : ℝ) : WithTop ℝ)

theorem primeElementFor_unit_mul_zpow_value
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π)
    (u : exponentialValuationSubring v) (hu : IsUnit u) (m : ℤ) :
    v ((u : K) * π ^ m) = ((m : ℝ) : WithTop ℝ)

theorem normalizedExponentialValuation_exists_unit_mul_zpow
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π x : K}
    (hπ : PrimeElementFor v π) (hx : x ≠ 0) :
    ∃ m : ℤ, ∃ u : exponentialValuationSubring v,
      IsUnit u ∧ x = (u : K) * π ^ m

theorem primeElementFor_unit_mul_zpow_unit_unique
    {K : Type*} [Field K] {v : ExponentialValuation K} {π : K}
    (hπ : PrimeElementFor v π) {m : ℤ}
    {u t : exponentialValuationSubring v}
    (h : (u : K) * π ^ m = (t : K) * π ^ m) :
    u = t

theorem primeElementFor_unit_mul_zpow_exponent_unique
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π)
    {m n : ℤ} {u t : exponentialValuationSubring v}
    (hu : IsUnit u) (ht : IsUnit t)
    (h : (u : K) * π ^ m = (t : K) * π ^ n) :
    m = n

theorem primeElementFor_unit_mul_zpow_unique
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π)
    {m n : ℤ} {u t : exponentialValuationSubring v}
    (hu : IsUnit u) (ht : IsUnit t)
    (h : (u : K) * π ^ m = (t : K) * π ^ n) :
    m = n ∧ u = t

theorem normalizedExponentialValuation_exists_unique_unit_mul_zpow
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π x : K}
    (hπ : PrimeElementFor v π) (hx : x ≠ 0) :
    ∃ m : ℤ, ∃ u : exponentialValuationSubring v,
      IsUnit u ∧ x = (u : K) * π ^ m ∧
        ∀ n : ℤ, ∀ t : exponentialValuationSubring v,
          IsUnit t → x = (t : K) * π ^ n → n = m ∧ t = u

theorem primeElementInValuationSubring_pow_value
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    v ((primeElementInValuationSubring v hπ : exponentialValuationSubring v) ^ n : K) =
      ((n : ℝ) : WithTop ℝ)

theorem exponentialMaxIdeal_eq_span_primeElement_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    exponentialMaxIdeal v =
      Ideal.span
        ({primeElementInValuationSubring v hπ} :
          Set (exponentialValuationSubring v))

theorem maximalIdeal_eq_span_primeElement_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    IsLocalRing.maximalIdeal (exponentialValuationSubring v) =
      Ideal.span
        ({primeElementInValuationSubring v hπ} :
          Set (exponentialValuationSubring v))

theorem span_primeElement_isMaximal_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    (Ideal.span
      ({primeElementInValuationSubring v hπ} :
        Set (exponentialValuationSubring v))).IsMaximal

theorem span_primeElement_isPrime_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    (Ideal.span
      ({primeElementInValuationSubring v hπ} :
        Set (exponentialValuationSubring v))).IsPrime

theorem primeElementInValuationSubring_prime_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    Prime (primeElementInValuationSubring v hπ)

theorem primeElementInValuationSubring_irreducible_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    Irreducible (primeElementInValuationSubring v hπ)

theorem exponentialMaxIdeal_pow_eq_span_primeElement_pow_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    (exponentialMaxIdeal v) ^ n =
      Ideal.span
        ({(primeElementInValuationSubring v hπ) ^ n} :
          Set (exponentialValuationSubring v))

def uniformizerPowerIdeal {O : Type*} [CommRing O] (π : O) (n : ℕ) : Ideal O

theorem uniformizerPowerIdeal_mem_iff_value_ge_of_pow_value
    {K : Type*} [Field K] (v : ExponentialValuation K)
    {π : K} (πR : exponentialValuationSubring v)
    (hπR : (πR : K) = π) {s : ℝ} (hπ0 : π ≠ 0)
    (hpow : ∀ n : ℕ, v (π ^ n) = (((n : ℝ) * s : ℝ) : WithTop ℝ))
    (n : ℕ) (x : exponentialValuationSubring v) :
    x ∈ uniformizerPowerIdeal πR n ↔
      (((n : ℝ) * s : ℝ) : WithTop ℝ) ≤ v (x : K)

theorem uniformizerPowerIdeal_le_ideal_of_mem_value_eq_of_pow_value
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {π : K} (πR : exponentialValuationSubring v)
    (hπR : (πR : K) = π) {s : ℝ} (hπ0 : π ≠ 0)
    (hpow : ∀ n : ℕ, v (π ^ n) = (((n : ℝ) * s : ℝ) : WithTop ℝ))
    {I : Ideal (exponentialValuationSubring v)} {n : ℕ}
    {x : exponentialValuationSubring v}
    (hxI : x ∈ I)
    (hxval : v (x : K) = (((n : ℝ) * s : ℝ) : WithTop ℝ)) :
    uniformizerPowerIdeal πR n ≤ I

theorem ideal_exists_min_value_of_nat_indexed_values
    {O α : Type*} [CommRing O] [Preorder α]
    (value : O → α) (weight : ℕ → α) (hweight : Monotone weight)
    (hvalue : ∀ x : O, x ≠ 0 → ∃ n : ℕ, value x = weight n)
    (I : Ideal O) (hI : I ≠ ⊥) :
    ∃ n : ℕ, ∃ x : O,
      x ∈ I ∧ x ≠ 0 ∧ value x = weight n ∧
        ∀ y : O, y ∈ I → y ≠ 0 → weight n ≤ value y

theorem uniformizerPowerIdeal_mem_iff_value_ge
    {K : Type*} [Field K] (v : ExponentialValuation K) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ)
    (x : exponentialValuationSubring v) :
    x ∈ uniformizerPowerIdeal (primeElementInValuationSubring v hπ) n ↔
      ((n : ℝ) : WithTop ℝ) ≤ v (x : K)

theorem exists_nat_index_of_nonneg_int_multiple
    {a : WithTop ℝ} {s : ℝ} (ha : 0 ≤ a) (hs : 0 < s)
    (h : ∃ m : ℤ, a = (((m : ℝ) * s : ℝ) : WithTop ℝ)) :
    ∃ n : ℕ, a = (((n : ℝ) * s : ℝ) : WithTop ℝ)

theorem normalizedExponentialValuation_subring_exists_nat_value
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v)
    {x : exponentialValuationSubring v} (hx : (x : K) ≠ 0) :
    ∃ n : ℕ, v (x : K) = ((n : ℝ) : WithTop ℝ)

theorem uniformizerPowerIdeal_le_ideal_of_mem_value_eq
    {K : Type*} [Field K] {v : ExponentialValuation K} {π : K}
    (hπ : PrimeElementFor v π)
    {I : Ideal (exponentialValuationSubring v)} {n : ℕ}
    {x : exponentialValuationSubring v}
    (hxI : x ∈ I)
    (hxval : v (x : K) = ((n : ℝ) : WithTop ℝ)) :
    uniformizerPowerIdeal (primeElementInValuationSubring v hπ) n ≤ I

theorem nonzero_ideal_eq_uniformizerPowerIdeal
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π)
    (I : Ideal (exponentialValuationSubring v)) (hI : I ≠ ⊥) :
    ∃ n : ℕ,
      I = uniformizerPowerIdeal (primeElementInValuationSubring v hπ) n

theorem normalizedExponentialValuationSubring_isPrincipalIdealRing
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    IsPrincipalIdealRing (exponentialValuationSubring v)

theorem normalizedExponentialValuationSubring_isDiscreteValuationRing
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) :
    IsDiscreteValuationRing (exponentialValuationSubring v)

def discretePrimeElementInValuationSubring
    {K : Type*} [Field K] (v : ExponentialValuation K)
    {π : K} {s : ℝ} (hs : 0 ≤ s) (hπ : v π = (s : WithTop ℝ)) :
    exponentialValuationSubring v

theorem discretePrimeElement_ne_zero_of_value
    {K : Type*} [Field K] (v : ExponentialValuation K)
    {π : K} {s : ℝ} (hπ : v π = (s : WithTop ℝ)) :
    π ≠ 0

theorem discretePrimeElement_pow_value
    {K : Type*} [Field K] (v : ExponentialValuation K)
    {π : K} {s : ℝ} (hπ : v π = (s : WithTop ℝ)) (n : ℕ) :
    v (π ^ n) = (((n : ℝ) * s : ℝ) : WithTop ℝ)

theorem discreteExponentialValuation_subring_exists_nat_value
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {s : ℝ} (hs : 0 < s)
    (hvalues : ∀ x : K, x ≠ 0 → ∃ m : ℤ,
      v x = (((m : ℝ) * s : ℝ) : WithTop ℝ))
    {x : exponentialValuationSubring v} (hx : (x : K) ≠ 0) :
    ∃ n : ℕ, v (x : K) = (((n : ℝ) * s : ℝ) : WithTop ℝ)

theorem discrete_uniformizerPowerIdeal_mem_iff_value_ge
    {K : Type*} [Field K] (v : ExponentialValuation K)
    {π : K} {s : ℝ} (hs : 0 < s) (hπ : v π = (s : WithTop ℝ))
    (n : ℕ) (x : exponentialValuationSubring v) :
    x ∈ uniformizerPowerIdeal
        (discretePrimeElementInValuationSubring v (le_of_lt hs) hπ) n ↔
      (((n : ℝ) * s : ℝ) : WithTop ℝ) ≤ v (x : K)

theorem discreteUniformizerPowerIdeal_le_ideal_of_mem_value_eq
    {K : Type*} [Field K] {v : ExponentialValuation K}
    {π : K} {s : ℝ} (hs : 0 < s) (hπ : v π = (s : WithTop ℝ))
    {I : Ideal (exponentialValuationSubring v)} {n : ℕ}
    {x : exponentialValuationSubring v}
    (hxI : x ∈ I)
    (hxval : v (x : K) = (((n : ℝ) * s : ℝ) : WithTop ℝ)) :
    uniformizerPowerIdeal
      (discretePrimeElementInValuationSubring v (le_of_lt hs) hπ) n ≤ I

theorem discreteExponentialValuationSubring_isPrincipalIdealRing
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : DiscreteExponentialValuation v) :
    IsPrincipalIdealRing (exponentialValuationSubring v)

theorem discreteExponentialValuationSubring_isDiscreteValuationRing
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : DiscreteExponentialValuation v) :
    IsDiscreteValuationRing (exponentialValuationSubring v)