Commit 2024-11-27 19:53 0aebe464
View on Github →refactor(Combinatorics/Additive): generalise Ruzsa's covering lemma to non-abelian groups (#19512) Also state it using a fixed real number and use semantic lemma names. This is much more useful in practice. From GrowthInGroups (LeanCamCombi)