Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2018P3

module

public import Mathlib.Algebra.Order.Star.Basic
public import Mathlib.Data.Nat.Choose.Sum
public import Mathlib.Data.Nat.Totient
public import Mathlib.NumberTheory.Padics.PadicVal.Basic

public section


/-!
# USA Mathematical Olympiad 2018, Problem 3

Let n ≥ 2 be an integer, and let {a₁, ..., aₘ} denote the m = φ(n) integers
less than n and relatively prime to n. Assume that every prime divisor of m
also divides n. Prove that m divides a₁ᵏ + ⋯ + aₘᵏ for every positive integer k.
-/

namespace Usa2018P3

theorem usa2018_p3 (n : ℕ) (hn : 2 ≤ n) (k : ℕ) (hk : 1 ≤ k)
    (h : ∀ p : ℕ, p.Prime → p ∣ n.totient → p ∣ n) :
    n.totient ∣ ∑ a ∈ (Finset.range n).filter (Nat.Coprime n), a ^ k := sorry

end Usa2018P3

File author(s): Kimi K3

This problem has a complete formalized solution.