feat(ring/localization): add fraction map for int to rat cast (#2921)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/rat/basic.lean

@@ -619,7 +619,7 @@ end casts
 lemma inv_def' {q : ℚ} : q⁻¹ = (q.denom : ℚ) / q.num :=
 by { conv_lhs { rw ←(@num_denom q) }, cases q, simp [div_num_denom] }
 
-@[simp] lemma mul_own_denom_eq_num {q : ℚ} : q * q.denom = q.num :=
+@[simp] lemma mul_denom_eq_num {q : ℚ} : q * q.denom = q.num :=
 begin
   suffices : mk (q.num) ↑(q.denom) * mk ↑(q.denom) 1 = mk (q.num) 1, by
   { conv { for q [1] { rw ←(@num_denom q) }}, rwa [coe_int_eq_mk, coe_nat_eq_mk] },

src/ring_theory/localization.lean

@@ -707,4 +707,30 @@ noncomputable def to_field [comm_ring K] (φ : fraction_map A K) : field K :=
   mul_inv_cancel := φ.mul_inv_cancel,
   inv_zero := dif_pos rfl, ..φ.to_integral_domain }
 
+/-- The cast from `int` to `rat` as a `fraction_map`. -/
+def int.fraction_map : fraction_map ℤ ℚ :=
+{ to_fun := coe,
+  map_units' :=
+  begin
+    rintro ⟨x, hx⟩,
+    rw [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero] at hx,
+    simpa only [is_unit_iff_ne_zero, int.cast_eq_zero, ne.def, subtype.coe_mk] using hx,
+  end,
+  surj' :=
+  begin
+    rintro ⟨n, d, hd, h⟩,
+    refine ⟨⟨n, ⟨d, _⟩⟩, rat.mul_denom_eq_num⟩,
+    rwa [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero, int.coe_nat_ne_zero_iff_pos]
+  end,
+  eq_iff_exists' :=
+  begin
+    intros x y,
+    rw [int.cast_inj],
+    refine ⟨by { rintro rfl, use 1 }, _⟩,
+    rintro ⟨⟨c, hc⟩, h⟩,
+    apply int.eq_of_mul_eq_mul_right _ h,
+    rwa [submonoid.mem_carrier, mem_non_zero_divisors_iff_ne_zero] at hc,
+  end,
+  ..int.cast_ring_hom ℚ }
+
 end fraction_map