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:

[Antoine Chambert-Loir]

Two late comments, @Yaël Dillies :

1. As the proof of docs#char_dvd_card_solutions_of_sum_lt indicates, the theorem for one polynomial and its version for a family are elementary equivalent.
2. There is a version of EGZ for integers: If $n>0$ is an integer, among $2n-1$ integers, one can find $n$ of them whose sum is divisible by $n$.

[Yaël Dillies]

1. How is that relevant to EGZ?
2. I am aware, and in fact I have an almost complete proof of this fact in LeanCamCombi.

[Yaël Dillies]

If you're interested in reviewing EGZ, I can PR it soon and tag you

[Antoine Chambert-Loir]

(For 1 : it is just that you say this might be the only application of the CW-theorem for several polynomials )

[Yaël Dillies]

Oh that's not what I meant. I meant this is the first application of CW, all versions included.

[Antoine Chambert-Loir]

Well, CW has a few classical applications!
One of them is the proof that all finite fields are commutative (using the reduced norm), or to the theory of quadratic forms over finite fields (which are thus automatically isotropic in dimension $\geq3$…)
There are also combinatorical applications : how many hyperplanes are needed to cover the affine space over a finite field? and if you insist that these hyperplanes avoid the origin?
And applications in code theory.
Maybe more importantly, it relates the geometric properties of an algebraic variety with the presence of rational points, and is directly a motivation to quite fundamental questions in arithmetic geometry (papers by Ax, Katz, Esnault, Fakhruddin-Rajan…)

[Yaël Dillies]

In mathlib! I mean first application in mathlib.

[Yaël Dillies]

Sorry, clearly I haven't been very clear :grinning:

[Antoine Chambert-Loir]

That's OK ! — I'm a bit too “milky soup” these times…