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)

Estimated changes