Kneser's Theorem and the Cauchy–Davenport Theorem

Mantas Bakšys 📧 and Angeliki Koutsoukou-Argyraki 📧

November 21, 2022


We formalise Kneser's Theorem in combinatorics following the proof from the 2014 paper A short proof of Kneser’s addition theorem for abelian groups by Matt DeVos. We also show a strict version of Kneser's Theorem as well as the Cauchy–Davenport Theorem as a corollary of Kneser's Theorem.


BSD License


Related publications

  • DeVos, M. (2014). A Short Proof of Kneser’s Addition Theorem for Abelian Groups. Combinatorial and Additive Number Theory, 39–41.
  • Nathanson, Melvyn B, Additive Number Theory: Inverse Problems and the Geometry of Sumsets, Springer-Verlag, 1996, vol. 165, Graduate Texts in Mathematics, isbn 978-0-387-94655-9
  • Ruzsa, Imre Z., Sumsets and Structure, Course notes, 2008, available on

Session Kneser_Cauchy_Davenport