exists_pow_lt_of_le_exp_neg_one — Mathlib

English

For any x with v(x) ≤ exp(−1) in a valued ring, there exists n such that v(x)^n is smaller than a prescribed unit γ.

Русский

Для любого x с v(x) ≤ exp(−1) в оцененном кольце существует неотрицательное число n такое, что v(x)^n меньше заданной единицы γ.

LaTeX

$$$\exists n\, (v(x))^n < γ$ для заданного γ ∈ ℤᵐ⁰ˣ и hx = v(x) ≤ exp(-1)$$

Lean4

theorem exists_pow_lt_of_le_exp_neg_one [Valued R ℤᵐ⁰] {x : R} (hx : v x ≤ exp (-1)) (γ : ℤᵐ⁰ˣ) : ∃ n, v x ^ n < γ :=
  by
  refine exists_pow_lt₀ (hx.trans_lt ?_) _
  rw [← exp_zero, exp_lt_exp]
  simp

Похожие утверждения