Commit 2023-12-19 12:55 5e71f8d0

View on Github →

feat: Ruzsa covering for sets (#8916) Add a version covering for Set α and Nat.card. From PFR

Estimated changes

Modified Mathlib/Combinatorics/Additive/RuzsaCovering.lean

added theorem Set.exists_subset_mul_div

Modified Mathlib/Data/Set/Card.lean

modified theorem Set.Nat.card_coe_set_eq