English
The localization of the integers by the submonoid of positive integers yields the rationals; i.e., IsLocalization(Submonoid.pos ℤ, ℚ).
Русский
Локализация целых по подмонаду положительных чисел даёт рациональные числа; то есть IsLocalization(слово положительных целых, \mathbb{Q}).
LaTeX
$$IsLocalization (Submonoid.pos \mathbb{Z}) \mathbb{Q}$$
Lean4
/-- As a corollary, `Rat` is also a localization at only positive integers. -/
instance : IsLocalization (Submonoid.pos ℤ) ℚ
where
map_units y := by simpa using y.prop.ne'
surj
z := by
obtain ⟨⟨x1, x2⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors ℤ) z
obtain hx2 | hx2 := lt_or_gt_of_ne (show x2.val ≠ 0 by simp)
· exact ⟨⟨-x1, ⟨-x2.val, by simpa using hx2⟩⟩, by simpa using hx⟩
· exact ⟨⟨x1, ⟨x2.val, hx2⟩⟩, hx⟩
exists_of_eq {x y} h := ⟨1, by simpa using Rat.intCast_inj.mp h⟩
