Kneser's Theorem and the Cauchy–Davenport Theorem

Mantas Bakšys 📧 and Angeliki Koutsoukou-Argyraki 📧

November 21, 2022

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 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.

License

BSD License

Topics

Related publications

  • DeVos, M. (2014). A Short Proof of Kneser’s Addition Theorem for Abelian Groups. Combinatorial and Additive Number Theory, 39–41. https://doi.org/10.1007/978-1-4939-1601-6_3
  • 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 https://www.math.cmu.edu/users/af1p/Teaching/AdditiveCombinatorics/Additive-Combinatorics.pdf

Session Kneser_Cauchy_Davenport

Depends on

Cite

× 
@article{Kneser_Cauchy_Davenport-AFP,
  author  = {Mantas Bakšys and Angeliki Koutsoukou-Argyraki},
  title   = {Kneser's Theorem and the Cauchy–Davenport Theorem},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Kneser_Cauchy_Davenport.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: