Mathlib theorem · Existing formal mathematics
ProofAtlas

Existing in Mathlib · Combinatorics and number theory

Cauchy–Davenport Theorem

Place two nonempty finite sets on the residues modulo a prime p and add every element of the first to every element of the second. After duplicate sums are merged, at least min(p, |S|+|T|−1) distinct residues remain.

Exact theorem

Exact Mathlib statement

lemma ZMod.cauchy_davenport {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) : min p (#s + #t - 1) ≤ #(s + t)

The theorem at a glance

Cauchy–Davenport at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

In a prime cyclic group, a nonempty sumset cannot stay smaller than min(p, |S|+|T|−1). Explanatory diagram.
Detailed visual description

The poster centers the sumset lower bound between two input residue circles and one expanded output circle. A short route strip presents prime cyclic order, the e-transform idea, preserved total input size, and the resulting lower bound without asserting equality.

Statement structure

From hypotheses to conclusion

Statement map for Cauchy–Davenport TheoremTwo nonempty subsets of a prime cyclic group have a sumset of size at least the smaller of p and |S|+|T|−1. The pinned upstream declaration is ZMod.cauchy_davenport. The exact checked statement is lemma ZMod.cauchy_davenport {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) : min p (#s + #t - 1) ≤ #(s + t).Mathematical readingTwo nonempty subsets ofa prime cyclic grouphave a sumset of size atleast the smaller of pand |S|+|T|−1.Pinned declarationmathlib ·ZMod.cauchy_davenportExact checked formlemmaZMod.cauchy_davenport {p: ℕ} (hp : p.Prime) {s t: Finset (ZMod p)} (hs :s.Nonempty) (ht :t.Nonempty) : min p (#s+ #t - 1) ≤ #(s + t)Statement map for Cauchy–Davenport TheoremTwo nonempty subsets of a prime cyclic group have a sumset of size at least the smaller of p and |S|+|T|−1. The pinned upstream declaration is ZMod.cauchy_davenport. The exact checked statement is lemma ZMod.cauchy_davenport {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) : min p (#s + #t - 1) ≤ #(s + t).Mathematical readingTwo nonempty subsets ofa prime cyclic grouphave a sumset of size atleast the smaller of pand |S|+|T|−1.Pinned declarationmathlib ·ZMod.cauchy_davenportExact checked formlemmaZMod.cauchy_davenport {p: ℕ} (hp : p.Prime) {s t: Finset (ZMod p)} (hs :s.Nonempty) (ht :t.Nonempty) : min p (#s+ #t - 1) ≤ #(s + t)

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Addition of two nonempty sets modulo a prime forces at least |S|+|T|−1 distinct sums, until all p residues are reached. Explanatory diagram.
Detailed visual description

Three aligned prime residue circles show two nonempty input selections and their deduplicated pointwise sumset. Fine addition chords connect representative pairs while a gold occupancy arc makes expansion and saturation at the full p-element circle visually distinct.

Why it matters

A mathematical landmark

Cauchy–Davenport is a foundational lower bound in additive combinatorics, showing that addition in a prime cyclic group forces finite sets to expand unless the whole group is already reached.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's nonempty-finset theorem in ZMod p for prime p. The pointwise sumset uses distinct residues, and the conclusion is the lower bound min(p, |s|+|t|−1) ≤ |s+t|. It is not an equality theorem and does not select Mathlib's more general group variants.

Source and local evidence

Where the theorem comes from

Existing declaration
ZMod.cauchy_davenport in mathlib
Relationship
The checked artifact is the upstream declaration itself
Local Lean evidence
artifact.library.mathlib.cauchy-davenport-theorem.v001
Source
Open the pinned upstream reference