Theorem Finset.ruzsa_covering_mul

Modification history

2024-11-27 19:53
Mathlib/Combinatorics/Additive/RuzsaCovering.lean
refactor(Combinatorics/Additive): generalise Ruzsa's covering lemma to non-abelian groups (#19512) …
Added Finset.ruzsa_covering_mulView on Github →