Commit 2023-02-22 09:22 ae05b307

View on Github →

feat: port Combinatorics.Additive.PluenneckeRuzsa (#2433)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

added theorem Finset.card_add_nsmul_le

added theorem Finset.card_div_mul_le_card_div_mul_card_div

added theorem Finset.card_div_mul_le_card_div_mul_card_mul

added theorem Finset.card_div_mul_le_card_mul_mul_card_div

added theorem Finset.card_div_mul_le_card_mul_mul_card_mul

added theorem Finset.card_mul_mul_card_le_card_mul_mul_card_mul

added theorem Finset.card_mul_mul_le_card_div_mul_card_div

added theorem Finset.card_mul_mul_le_card_div_mul_card_mul

added theorem Finset.card_mul_mul_le_card_mul_mul_card_div

added theorem Finset.card_mul_pow_le

added theorem Finset.card_pow_div_pow_le'

added theorem Finset.card_pow_div_pow_le

added theorem Finset.card_pow_le'

added theorem Finset.card_pow_le

added theorem Finset.mul_pluennecke_petridis