instEncodable — Mathlib

English

The rationals admit an encoding into natural numbers; i.e., they are encodable.

Русский

Рациональные числа допускают кодирование в натуральные числа; т.е. они кодируемы.

LaTeX

$$Encodable \mathbb{Q}$$

Lean4

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⟩

Похожие утверждения