Topological results for integer-valued rings

This file contains topological results for valuation rings taking values in the multiplicative integers with zero adjoined. These are useful for cases where there is a Valued R ℤₘ₀ instance but no canonical base with which to embed this into NNReal.

theorem Valued.tendsto_zero_pow_of_v_lt_one {R : Type u_1} {Γ₀ : Type u_2} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀] [Valued R Γ₀] {x : R} (hx : v x < 1) : Filter.Tendsto (fun (n : ℕ) => x ^ n) Filter.atTop (nhds 0)

theorem Valued.tendsto_zero_pow_of_le_exp_neg_one {R : Type u_1} [Ring R] [Valued R (WithZero (Multiplicative ℤ))] {x : R} (hx : v x ≤ WithZero.exp (-1)) : Filter.Tendsto (fun (n : ℕ) => x ^ n) Filter.atTop (nhds 0)

In a ℤᵐ⁰-valued ring, powers of x tend to zero if v x ≤ exp (-1).

theorem Valued.exists_pow_lt_of_le_exp_neg_one {R : Type u_1} [Ring R] [Valued R (WithZero (Multiplicative ℤ))] {x : R} (hx : v x ≤ WithZero.exp (-1)) (γ : (WithZero (Multiplicative ℤ))ˣ) : ∃ (n : ℕ), v x ^ n < ↑γ