mathlib3 documentation

mathlib-archive / imo.imo1964_q1

IMO 1964 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

(a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.

(b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.

We define a predicate for the solutions in (a), and prove that it is the set of positive integers which are a multiple of 3.

Intermediate lemmas #

The question #

def imo1964_q1.problem_predicate (n : ) :
theorem imo1964_q1b (n : ) :
¬7 2 ^ n + 1