exists_mem_range_of_norm_rat_le_one

English

If p is prime and r ∈ ℚ with ||r|| ≤ 1, there exists an integer n with 0 ≤ n < p and ||⟨r⟩ − n|| < 1.

Русский

Если p простое и r ∈ ℚ с ||r|| ≤ 1, существует целое n с 0 ≤ n < p и ||⟨r⟩ − n|| < 1.

LaTeX

$$$\\\\exists n \\\\in \\\\mathbb{Z}, 0 \\le n < p \\\\land \\\\| (\\\\langle r,h\\\\rangle - n) \\\\|_p < 1$$$

Lean4

theorem exists_mem_range_of_norm_rat_le_one (h : ‖(r : ℚ_[p])‖ ≤ 1) :
    ∃ n : ℤ, 0 ≤ n ∧ n < p ∧ ‖(⟨r, h⟩ - n : ℤ_[p])‖ < 1 :=
  ⟨modPart p r, modPart_nonneg _, modPart_lt_p _, norm_sub_modPart _ h⟩

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