English
For any p prime and PadicInt x, there exists n with n < p and x - n in the maximal ideal.
Русский
Для любого p-простого и PadicInt x существует n < p такой, что x - n лежит в максимальном идеале.
LaTeX
$$$\\\\exists n \\\\in \\\\mathbb{N}, n < p \\\\land x - n \\\\in \\text{maximalIdeal}(\\\\mathbb{Z}_{p})$$$
Lean4
theorem exists_mem_range : ∃ n : ℕ, n < p ∧ x - n ∈ maximalIdeal ℤ_[p] :=
by
simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one
have H : ‖(r : ℚ_[p])‖ ≤ 1 := by
rw [norm_sub_rev] at hr
calc
_ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
_ ≤ _ := (Padic.nonarchimedean _ _)
_ ≤ _ := max_le (le_of_lt hr) x.2
obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H
lift n to ℕ using hzn
use n
constructor
· exact mod_cast hnp
simp only [norm_def, coe_sub, coe_natCast] at hn ⊢
rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]
apply lt_of_le_of_lt (Padic.nonarchimedean _ _)
apply max_lt hr
simpa using hn
