## 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