mathlib3

4aab2abc - feat(combinatorics/additive/pluennecke_ruzsa): The Plünnecke-Ruzsa inequality (#15440)

feat(combinatorics/additive/pluennecke_ruzsa): The Plünnecke-Ruzsa inequality (#15440) Prove the Ruzsa triangle inequalities, the Plünnecke-Petridis lemma, and the Plünnecke-Ruzsa inequality. Co-authored-by: georgeshakan <george.shakan@gmail.com>