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 ℤ))ˣ)
: