Theorem Finset.exists_subset_mul_div

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) …
Deleted Finset.exists_subset_mul_divView on Github →
2023-02-06 07:04
Mathlib/Combinatorics/Additive/RuzsaCovering.lean
feat: port Combinatorics.Additive.RuzsaCovering (#2065)
Added Finset.exists_subset_mul_divView on Github →