Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2006P5

import Mathlib.Algebra.Polynomial.Roots
import Mathlib.Dynamics.PeriodicPts

/-!
# International Mathematical Olympiad 2006, Problem 5

Let $P(x)$ be a polynomial of degree $n>1$ with integer coefficients, and let $k$ be a positive
integer. Consider the polynomial $Q(x) = P(P(\ldots P(P(x))\ldots))$, where $P$ occurs $k$ times.
Prove that there are at most $n$ integers $t$ such that $Q(t)=t$.
-/

open Function Polynomial

namespace Imo2006P5

theorem imo2006_p5 {P : Polynomial ℤ} (hP : 1 < P.natDegree) {k : ℕ} (hk : 0 < k) :
    (P.comp^[k] X - X).roots.toFinset.card ≤ P.natDegree := sorry


end Imo2006P5

File author(s): Violeta Hernández Palacios

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2006P5.lean.