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

- Mathematics/Combinatorics

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

- Kneser_Cauchy_Davenport_preliminaries
- Kneser_Cauchy_Davenport_main_proofs

### Depends on

- A Case Study in Basic Algebra
- The Plünnecke-Ruzsa Inequality

## Cite

×

Kneser_Cauchy_Davenport-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Dec 1, 2022 : Isabelle2022