Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A Generalization of the Cauchy...


view this post on Zulip Email Gateway (Dec 27 2024 at 12:31):

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