mathlib

1a54e4da - feat(combinatorics/additive/ruzsa_covering): The Ruzsa covering lemma (#14697)

feat(combinatorics/additive/ruzsa_covering): The Ruzsa covering lemma (#14697) Prove the Ruzsa covering lemma, which says that a finset `s` can be covered using at most $\frac{|s + t|}{|t|}$ copies of `t - t`. Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>