Documentation

Archive.Imo.Imo2019Q1

IMO 2019 Q1 #

Determine all functions f : ℤ → ℤ such that, for all integers a and b, f(2a) + 2f(b) = f(f(a+b)).

The desired theorem is that either:

Note that there is a much more compact proof of this fact in Isabelle/HOL

theorem imo2019_q1 (f : ) :
(∀ (a b : ), f (2 * a) + 2 * f b = f (f (a + b))) f = 0 ∃ (c : ), f = fun (x : ) => 2 * x + c