The Cauchy-Davenport theorem as a corollary of Kneser's lemma

This file proves the Cauchy-Davenport theorem as a corollary of Kneser's lemma.

Main declarations

• ZMod.min_le_card_add': The Cauchy-Davenport theorem.

Tags

additive combinatorics, number theory, sumset, cauchy-davenport

theorem ZMod.cauchy_davenport' {p : ℕ} (hp : Nat.Prime p) {s t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) : min p (s.card + t.card - 1) ≤ (s + t).card

The Cauchy-Davenport Theorem.