mathlib3 documentation

mathlib-archive / imo.imo1959_q1

IMO 1959 Q1 #

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

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 imo1959_q1.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)