Documentation

Archive.Imo.Imo1959Q1

IMO 1959 Q1 #

Prove that the fraction (21n+4)/(14n+3) is irreducible for every natural number n.

Since Lean doesn't have a concept of "irreducible fractions" per se, we just formalize this as saying the numerator and denominator are relatively prime.

theorem Imo1959Q1.calculation (n : ) (k : ) (h1 : k 21 * n + 4) (h2 : k 14 * n + 3) :
k 1
theorem imo1959_q1 (n : ) :
(21 * n + 4).Coprime (14 * n + 3)