Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Kneser's Theorem and the Cauch...

Email Gateway (Dec 01 2022 at 13:37):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

there is another new AFP entry today:

Kneser's Theorem and the Cauchy–Davenport Theorem
by Mantas Bakšys and Angeliki Koutsoukou-Argyraki

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.

https://www.isa-afp.org/entries/Kneser_Cauchy_Davenport.html

Enjoy,
René

Last updated: Jan 04 2025 at 20:18 UTC