English
An element x of a division ring that is integral over ℤ is rational if and only if it is equal to an integer. More precisely, x is equal to some rational q if and only if x equals some integer k.
Русский
Элемент x поля, являющийся целостным относительно ℤ, рационален тогда и только тогда, когда он равен целому числу; точнее, существует q ∈ ℚ с x = q ⇔ существует k ∈ ℤ с x = k.
LaTeX
$$$\\exists q \\in \\mathbb{Q},\\ x = q \\quad\\Leftrightarrow\\quad \\exists k \\in \\mathbb{Z},\\ x = k$$$
Lean4
theorem exists_int_iff_exists_rat (h₁ : IsIntegral ℤ x) : (∃ q : ℚ, x = q) ↔ ∃ k : ℤ, x = k :=
by
refine ⟨?_, fun ⟨w, h⟩ ↦ ⟨w, by simp [h]⟩⟩
rintro ⟨q, rfl⟩
rw [ratCast_iff] at h₁
peel IsIntegrallyClosed.algebraMap_eq_of_integral h₁ with h
simp [← h]
