English
Let S be a subfield of a division ring K. Then every rational number q, when viewed inside K, lies in S; i.e. the image of ℚ under the canonical embedding into K is contained in every subfield S of K.
Русский
Пусть S — подполе наддела K. Тогда действительное изображение рациональных чисел в K содержится в S; то есть образ ℚ в K лежит внутри любого подполе S ⊆ K.
LaTeX
$$$\\\\forall S \\\\subseteq K \\,\\\\forall q \\\\in \mathbb{Q}, \\\\,(q : K) \\\\in S$$$
Lean4
@[simp, aesop safe (rule_sets := [SetLike])]
theorem ratCast_mem (s : S) (q : ℚ) : (q : K) ∈ s := by
simpa only [Rat.cast_def] using div_mem (intCast_mem s q.num) (natCast_mem s q.den)