The rationals are encodable. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
As a consequence we also get the instance countable ℚ.
This is kept separate from data.rat.defs in order to minimize imports.
@[protected, instance]
Equations
- rat.encodable = encodable.of_equiv (Σ (n : ℤ), {d // 0 < d ∧ n.nat_abs.coprime d}) {to_fun := λ (_x : ℚ), rat.encodable._match_1 _x, inv_fun := λ (_x : Σ (n : ℤ), {d // 0 < d ∧ n.nat_abs.coprime d}), rat.encodable._match_2 _x, left_inv := rat.encodable._proof_1, right_inv := rat.encodable._proof_2}
- rat.encodable._match_1 {num := a, denom := b, pos := c, cop := d} = ⟨a, ⟨b, _⟩⟩
- rat.encodable._match_2 ⟨a, ⟨b, _⟩⟩ = {num := a, denom := b, pos := c, cop := d}