feat: port Data.Rat.Encodable (#1569)

Mathlib.lean

@@ -355,6 +355,7 @@ import Mathlib.Data.Quot
 import Mathlib.Data.Rat.Basic
 import Mathlib.Data.Rat.Cast
 import Mathlib.Data.Rat.Defs
+import Mathlib.Data.Rat.Encodable
 import Mathlib.Data.Rat.Floor
 import Mathlib.Data.Rat.Init
 import Mathlib.Data.Rat.Lemmas

Mathlib/Data/Rat/Encodable.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+
+! This file was ported from Lean 3 source module data.rat.encodable
+! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Logic.Encodable.Basic
+import Mathlib.Data.Nat.GCD.Basic
+import Mathlib.Data.Rat.Init
+
+/-! # The rationals are `Encodable`.
+
+As a consequence we also get the instance `Countable ℚ`.
+
+This is kept separate from `Data.Rat.Defs` in order to minimize imports.
+-/
+
+
+namespace Rat
+
+instance : Encodable ℚ :=
+  Encodable.ofEquiv (Σn : ℤ, { d : ℕ // 0 < d ∧ n.natAbs.coprime d })
+    ⟨fun ⟨a, b, c, d⟩ => ⟨a, b, Nat.pos_of_ne_zero c, d⟩,
+      fun ⟨a, b, c, d⟩ => ⟨a, b, Nat.pos_iff_ne_zero.mp c, d⟩,
+      fun _ => rfl, fun ⟨_, _, _, _⟩ => rfl⟩
+
+end Rat