Ruzsa's covering lemma #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file proves the Ruzsa covering lemma. This says that, for
t finsets, we can cover
with at most
(s + t).card / t.card copies of
t - t.
Merge this file with other prerequisites to Freiman's theorem once we have them.