Erdős–Ginzburg–Ziv theorem

Stream: maths

[Yaël Dillies]

As a followup to Kneser's addition theorem, I thought I would give a stab at Erdős–Ginzburg–Ziv, which says that among any $2p - 1$ elements of $ℤ/pℤ$ we can find $p$ elements of sum zero.

[Yaël Dillies]

And I just finished the proof! #18063

/-- The **Erdős–Ginzburg–Ziv theorem**: Any (not necessarily distinct) `2 * p - 1` elements of
`zmod p` contain `p` elements whose sum is zero. -/
lemma zmod.exists_le_sum_eq_zero {p : ℕ} [fact p.prime] {s : multiset (zmod p)} (hs : s.card = 2 * p - 1) :
   ∃ t ≤ s, t.card = p ∧ t.sum = 0 :=
...

#print axioms zmod.exists_le_sum_eq_zero
/-
propext
quot.sound
classical.choice
-/

[Yaël Dillies]

This to me is quite interesting, because I used the Chevalley-Warning proof, and AFAIK this is the first ever application of docs#char_dvd_card_solutions_family.

[Yaël Dillies]

Thank you, 2019 @Johan Commelin, for proving Chevalley-Warning :smile:

[Johan Commelin]

@Yaël Dillies Your welcome! :smiley: