From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce (with apologies for the delay) a contribution by Mantas Bakšys: A Generalization of the Cauchy–Davenport theorem.
The Cauchy--Davenport theorem is a fundamental result in additive combinatorics. It was originally independently discovered by Cauchy and Davenport and has been formalized in the AFP entry Kneser's Theorem and the Cauchy–Davenport Theorem as a corollary of Kneser's theorem. More recently, many generalizations of this theorem have been found. In this entry, we formalise a generalization due to DeVos, which proves the theorem in a non-abelian setting.
https://www.isa-afp.org/entries/Generalized_Cauchy_Davenport.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC