## Stream: new members

### Topic: all rational numbers whose denominators are a power of 2

#### Lars Ericson (Dec 24 2020 at 04:15):

I'm having trouble expressing "all rational numbers whose denominators are 1 or a power of 2". This is my first pass:

import data.rat.basic
import ring_theory.coprime
def binrat := {x : ℚ // ∃ (a : ℕ ) (b : ℕ ), b ≥ 0 ∧ (is_coprime a (2^b)) ∧  x = ⟨ a , 2^b ⟩ }


I'm getting error

type mismatch at application
x = rat.mk' ↑a (2 ^ b)
term
rat.mk' ↑a (2 ^ b)
has type
0 < 2 ^ b → ↑a.nat_abs.coprime (2 ^ b) → ℚ
but is expected to have type
ℚ


#### Yakov Pechersky (Dec 24 2020 at 04:35):

Why not

import data.rat.basic

def binrat := {x : ℚ // ∃ (p : ℕ), x.denom = 2 ^ p }


?

#### Mario Carneiro (Dec 24 2020 at 06:21):

Yeah, the author is being a bit silly there. Of course 1 is a power of 2

#### Mario Carneiro (Dec 24 2020 at 06:23):

@Lars Ericson That's maybe an example of what I was talking about earlier. The mathematician is writing for a human audience, which may not find it obvious that 1 is a power of 2 and so explicitly called it out. When formalizing, you definitely want to get rid of those junk disjuncts because they will only make the predicate harder to manipulate

#### Johan Commelin (Dec 24 2020 at 06:24):

@Lars Ericson rational numbers are not pairs of two natural numbers.

Last updated: May 10 2021 at 23:11 UTC