English
In a division ring k of characteristic zero, if n divides m in ℤ, then the cast of the quotient m/n to k equals the quotient in k: ((m/n) : ℤ) cast to k equals m/n in k, with nonzero denominator treated safely.
Русский
В делимой на характер ноль кольце k, если n делит m в ℤ, то каст такого отношения m/n в k равен отношению в k.
LaTeX
$$$\\forall m,n\\in\\mathbb{Z},\\ n\\neq 0\\Rightarrow ((m/n:\\mathbb{Z}):\\,k) = m/n$$$
Lean4
@[simp, norm_cast]
theorem cast_div_charZero {k : Type*} [DivisionRing k] [CharZero k] {m n : ℤ} (n_dvd : n ∣ m) :
((m / n : ℤ) : k) = m / n := by
rcases eq_or_ne n 0 with (rfl | hn)
· simp [Int.ediv_zero]
·
exact
cast_div n_dvd
(cast_ne_zero.mpr hn)
-- Necessary for confluence with `ofNat_ediv` and `cast_div_charZero`.
