English
For every integer n, the rational value of n / n equals the rational n / n (with the special case n = 0 giving 0/0 treated consistently). In particular, (n / n : ℤ) maps to the same rational as n / n.
Русский
Для любого целого числа n рациональное значение n/n равно рациональному n/n (с учетом случая n=0 как единичному делению).
LaTeX
$$$\\forall n \\in \\mathbb{Z},\\ ((n / n : \\mathbb{Z}) : \\mathbb{Q}) = n / n$$$
Lean4
@[norm_cast]
theorem intCast_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n :=
by
by_cases hn : n = 0
· subst hn
simp only [Int.cast_zero, zero_div, Int.ediv_zero]
· have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
simp only [Int.ediv_self hn, Int.cast_one, div_self this]
