English
Let K be a division ring. For any q ∈ ℚ≥0, the image of q via the cast from ℚ to K equals the cast of q via K, i.e., ((q : ℚ) : K) = (q : K).
Русский
Пусть K — кольцо деления. Для любого q ∈ ℚ≥0 образ q через приведение из ℚ в K совпадает с прямым приведением q в K: ((q : ℚ) : K) = (q : K).
LaTeX
$$$ ∀ K [DivisionRing K], ((q : \mathbb{Q}) : K) = (q : K). $$$
Lean4
@[simp, norm_cast]
theorem cast_nnratCast {K} [DivisionRing K] (q : ℚ≥0) : ((q : ℚ) : K) = (q : K) :=
by
rw [Rat.cast_def, NNRat.cast_def, NNRat.cast_def]
have hn := @num_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
on_goal 1 => have hd := @den_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
case hdp => simpa only [Int.natCast_pos] using q.den_pos
simp only [Int.cast_natCast, Nat.cast_inj] at hn hd
rw [hn, hd, Int.cast_natCast]
