IMO 2016 A4

Let $M$ be an integral multiplicative monoid with a cancellative, distributive addition. Find all functions $f : M → M$ such that, for all $x, y ∈ M$, $$ x f(x^2) f(f(y)) + f(y f(x)) = f(xy) \left(f(f(y^2)) + f(f(x^2))\right). $$

def IMOSL.IMO2016A4.good {M : Type u_1} [Mul M] [Add M] (f : M → M) : Prop

Equations

• IMOSL.IMO2016A4.good f = ∀ (x y : M), x * f (x * x) * f (f y) + f (y * f x) = f (x * y) * (f (f (y * y)) + f (f (x * x)))

class IMOSL.IMO2016A4.CancelCommDistribMonoid (M : Type u_1) extends CancelCommMonoid M, Distrib M : Type u_1

• mul : M → M → M
• mul_assoc (a b c : M) : a * b * c = a * (b * c)
• one : M
• one_mul (a : M) : 1 * a = a
• mul_one (a : M) : a * 1 = a
• npow : ℕ → M → M
• npow_zero (x : M) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : M) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• mul_comm (a b : M) : a * b = b * a
• mul_left_cancel (a : M) : IsLeftRegular a
• add : M → M → M
• left_distrib (a b c : M) : a * (b + c) = a * b + a * c
• right_distrib (a b c : M) : (a + b) * c = a * c + b * c

theorem IMOSL.IMO2016A4.inv'_is_good {M : Type u_1} [CancelCommDistribMonoid M] {f : M → M} (h : ∀ (x : M), x * f x = 1) : good f

theorem IMOSL.IMO2016A4.good_imp_inv' {M : Type u_1} [CancelCommDistribMonoid M] [IsCancelAdd M] {f : M → M} (hf : good f) (x : M) : x * f x = 1

theorem IMOSL.IMO2016A4.final_solution {M : Type u_1} [CancelCommDistribMonoid M] [IsCancelAdd M] {f : M → M} : good f ↔ ∀ (x : M), x * f x = 1

Final solution