Commit 2024-08-16 17:37 249c5361

View on Github →

feat: Doubling and difference constants of two finsets (#15882) Define the doubling and difference constants of two finsets in a group. The doubling and difference constants being small are one way to measure how close a set is from being a subgroup. This makes it a central concept in additive combinatorics and related fields. From LeanAPAP

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Additive/DoublingConst.lean

added theorem Finset.card_mul_cast_addConst

added theorem Finset.card_mul_cast_divConst

added theorem Finset.card_mul_cast_mulConst

added theorem Finset.card_mul_cast_subConst

added theorem Finset.card_mul_divConst

added theorem Finset.card_mul_mulConst

added theorem Finset.cast_addConst

added theorem Finset.cast_addConst_mul_card

added theorem Finset.cast_divConst

added theorem Finset.cast_divConst_mul_card

added theorem Finset.cast_mulConst

added theorem Finset.cast_mulConst_mul_card

added theorem Finset.cast_subConst

added theorem Finset.cast_subConst_mul_card

added def Finset.divConst

added theorem Finset.divConst_empty_left

added theorem Finset.divConst_empty_right

added theorem Finset.divConst_inv_left

added theorem Finset.divConst_inv_right

added theorem Finset.divConst_le_inv_dens

added theorem Finset.divConst_le_mulConst_sq

added theorem Finset.divConst_mul_card

added def Finset.mulConst

added theorem Finset.mulConst_empty_left

added theorem Finset.mulConst_empty_right

added theorem Finset.mulConst_inv_left

added theorem Finset.mulConst_inv_right

added theorem Finset.mulConst_le_divConst_sq

added theorem Finset.mulConst_le_inv_dens

added theorem Finset.mulConst_mul_card