Theorems · Theorem · number theory

cauchy_davenport_minOrder_mul

∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
  s.Nonempty → t.Nonempty → min (Monoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card

A generalisation of the Cauchy-Davenport theorem to arbitrary groups. The size of s * t is lower-bounded by |s| + |t| - 1 unless this quantity is greater than the size of the smallest subgroup.

Defined in

Mathlib.Combinatorics.Additive.CauchyDavenport

Cited by

1 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEq