Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2018P6

module

public import Mathlib.Algebra.Order.Field.Basic
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Rat.Star
public import Mathlib.GroupTheory.Perm.Fin
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas

public section


/-!
# USA Mathematical Olympiad 2018, Problem 6

Let $a_n$ be the number of permutations $(x_1, x_2, \ldots, x_n)$ of the numbers
$(1, 2, \ldots, n)$ such that the $n$ ratios $\frac{x_k}{k}$ for $1 \le k \le n$
are all distinct. Prove that $a_n$ is odd for all $n \ge 1$.
-/

namespace Usa2018P6

open Equiv Finset Function

/-- Summed `Nat.ModEq` over a finset. -/
lemma sum_modEq_of_forall {ι : Type*} [DecidableEq ι] (s : Finset ι) (f g : ι → ℕ)
    (h : ∀ i ∈ s, f i ≡ g i [MOD 2]) : (∑ i ∈ s, f i) ≡ (∑ i ∈ s, g i) [MOD 2] := by
  induction s using Finset.induction with
  | empty => exact Nat.ModEq.rfl
  | insert a s has ih =>
    rw [Finset.sum_insert has, Finset.sum_insert has]
    exact Nat.ModEq.add (h a (Finset.mem_insert_self a s))
      (ih (fun i hi => h i (Finset.mem_insert_of_mem hi)))

/-- USAMO 2018, Problem 6: the number of permutations of `(1, …, n)` whose ratios
`xₖ/k` are all distinct is odd for every `n ≥ 1`. -/
theorem usa2018_p6 (n : ℕ) (hn : 1 ≤ n) :
    Odd (Fintype.card {σ : Equiv.Perm (Fin n) // Valid σ}) := sorry

end Usa2018P6

File author(s): Kimi K3

This problem has a complete formalized solution.