Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1977P1

module

public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.Field.GeomSum
public import Mathlib.Algebra.Polynomial.Div
public import Mathlib.Algebra.Polynomial.FieldDivision
public import Mathlib.Algebra.Polynomial.Roots
public import Mathlib.Data.PNat.Basic
public import Mathlib.Algebra.Polynomial.Basic
public import Mathlib.RingTheory.RootsOfUnity.Complex
public import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

public section


/-!
# USA Mathematical Olympiad 1977, Problem 1

Determine all pairs of positive integers (m, n) such that

  1 + x ^ n + x ^ (2 * n) + ... + x ^ (m * n)

is divisible by

  1 + x + x ^ 2 + ... + x ^ m.
-/

namespace Usa1977P1

open Polynomial

noncomputable def geomSumStep (m n : ℕ+) : ℤ[X] :=
  ∑ k ∈ Finset.range (m + 1), X ^ (k * n : ℕ)

noncomputable def geomSum (m : ℕ+) : ℤ[X] :=
  ∑ k ∈ Finset.range (m + 1), X ^ k

/- determine -/ abbrev solution_set : Set (ℕ+ × ℕ+) := sorry

theorem usa1977_p1 (m n : ℕ+) :
    (m, n) ∈ solution_set ↔ geomSum m ∣ geomSumStep m n := sorry

end Usa1977P1

File author(s): Karl Mehltretter, Kimi K3

This problem has a complete formalized solution.