IMO 2019 Q1 #

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

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 = λ (x : ℤ), 2 * x + c