English
The rationals are the fraction field of the integers; i.e., the canonical localization of \mathbb{Z} by nonZeroDivisors(\mathbb{Z}) equals \mathbb{Q}.
Русский
Рациональные числа — это поле дробей над целыми; то есть локализация \mathbb{Z} по ненулевым делителям равна \mathbb{Q}.
LaTeX
$$$\text{IsFractionRing}(\mathbb{Z}, \mathbb{Q})$$$
Lean4
/-- The cast from `Int` to `Rat` as a `FractionRing`. -/
instance isFractionRing : IsFractionRing ℤ ℚ
where
map_units := by
rintro ⟨x, hx⟩
rw [mem_nonZeroDivisors_iff_ne_zero] at hx
simpa only [eq_intCast, isUnit_iff_ne_zero, Int.cast_eq_zero, Ne, Subtype.coe_mk] using hx
surj := by
rintro ⟨n, d, hd, h⟩
refine ⟨⟨n, ⟨d, ?_⟩⟩, Rat.mul_den_eq_num _⟩
rw [mem_nonZeroDivisors_iff_ne_zero, Int.natCast_ne_zero_iff_pos]
exact Nat.zero_lt_of_ne_zero hd
exists_of_eq
{x y} := by
rw [eq_intCast, eq_intCast, Int.cast_inj]
rintro rfl
use 1
