IMO 2019 Q1 #
Determine all functions
f : ℤ → ℤ such that, for all integers
f(2a) + 2f(b) = f(f(a+b)).
The desired theorem is that either:
f = fun _ ↦ 0
∃ c, f = fun x ↦ 2 * x + c
Note that there is a much more compact proof of this fact in Isabelle/HOL