Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1997P3

module

public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Int
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Polynomial.Div
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Analysis.Normed.Ring.Lemmas
public import Mathlib.Data.Int.Star

public section


/-!
# USA Mathematical Olympiad 1997, Problem 3

Prove that for any integer n, there exists a unique polynomial Q with
coefficients in {0, 1, ..., 9} such that Q(-2) = Q(-5) = n.
-/

namespace Usa1997P3

open Polynomial

theorem usa1997_p3 (n : ℤ) :
    ∃! Q : ℤ[X], (∀ i, 0 ≤ Q.coeff i ∧ Q.coeff i ≤ 9) ∧
      Q.eval (-2) = n ∧ Q.eval (-5) = n := sorry

end Usa1997P3

File author(s): Kimi K3

This problem has a complete formalized solution.