**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

We formalise Plünnecke's inequality and the Plünnecke-Ruzsa
inequality, following the notes by Timothy Gowers: "Introduction
to Additive Combinatorics" (2022) for the University of
Cambridge. To this end, we first introduce basic definitions and prove
elementary facts on sumsets and difference sets. Then, we show two
versions of the Ruzsa triangle inequality. We follow with a proof due
to Petridis.