Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1976P5

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.CStarAlgebra.Classes
public import Mathlib.RingTheory.RootsOfUnity.Complex
public import Mathlib.RingTheory.SimpleRing.Principal
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1976, Problem 5

The polynomials a(x), b(x), c(x), d(x) satisfy
a(x⁵) + x·b(x⁵) + x²·c(x⁵) = (1 + x + x² + x³ + x⁴)·d(x).
Show that a(x) has the factor (x - 1).
-/

namespace Usa1976P5

open Polynomial

theorem usa1976_p5 (a b c d : Polynomial ℂ)
    (h : a.comp (X ^ 5) + X * b.comp (X ^ 5) + X ^ 2 * c.comp (X ^ 5) =
        (1 + X + X ^ 2 + X ^ 3 + X ^ 4) * d) :
    X - C 1 ∣ a := sorry

end Usa1976P5

File author(s): Kimi K3

This problem has a complete formalized solution.