Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2018P4

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# USA Mathematical Olympiad 2018, Problem 4

Let p be a prime, and let a₁, ..., aₚ be integers. Show that there exists an integer k
such that the numbers

  a₁ + k, a₂ + 2k, ..., aₚ + pk

produce at least ½p distinct remainders upon division by p.
-/

namespace Usa2018P4

open Finset

/-- We index by `Fin p` instead of `{1, ..., p}` (the map `i ↦ i mod p` is a bijection
`{1, ..., p} ≃ Fin p` sending `p ↦ 0`, and `p * k ≡ 0 (mod p)`, so the families of
remainders coincide), we work directly with remainders in `ZMod p`, and the conclusion
`p ≤ 2 * N` is the integral form of "`N ≥ p / 2` distinct remainders". -/
theorem usa2018_p4 (p : ℕ) (hp : p.Prime) (a : Fin p → ℤ) :
    ∃ k : ℤ, p ≤ 2 * (Finset.univ.image fun i : Fin p ↦
      (a i : ZMod p) + ((i : ℕ) : ZMod p) * (k : ZMod p)).card := sorry

end Usa2018P4

File author(s): Kimi K3

This problem has a complete formalized solution.