English
For any division ring with characteristic zero, a rational number q embeds into the ring as an integral element if and only if its image is integral over ℤ in the ambient division ring.
Русский
Для делимого кольца характеристика которого ноль: число q ∈ ℚ является целостным над ℤ в этом кольце тогда и только тогда, когда q как элемент кольца целостен над ℤ.
LaTeX
$$$\\forall \\alpha \\text{ division ring},\\ Char(\\alpha)=0,\\ (q:\\mathbb{Q}) \\,\\Rightarrow \\, IsIntegral(\\mathbb{Z}, q) \\iff IsIntegral(\\mathbb{Z}, q^{\\mathsf{cast}})$$$
Lean4
@[simp]
theorem ratCast_iff : IsIntegral ℤ (q : α) ↔ IsIntegral ℤ q :=
isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective ℚ α)
