Commit 2023-12-08 15:24 75d413be
View on Github →feat: The Cauchy-Davenport theorem (#8429)
This PR proves a very general version of the Cauchy-Davenport theorem, namely a lower bound on the size of the product s * t of two finsets in terms of the size of s and t.
We also provide a different proof for linearly ordered cancellative semigroups.