Commit 2024-05-30 19:52 de57ce8a

View on Github →

feat: Dissociation of sets (#10555) In additive combinatorics, a pretty standard tool called Chang's lemma uses a version of linear independence and linear span with "scalars" restricted to {-1, 0, 1}. This PR defines those analogs, known as dissociation and span in the literature. From LeanAPAP

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Additive/Dissociation.lean

added theorem Finset.exists_subset_mulSpan_card_le_of_forall_mulDissociated

added theorem Finset.mem_mulSpan

added def Finset.mulSpan

added theorem Finset.prod_div_prod_mem_mulSpan

added theorem Finset.subset_mulSpan

added theorem MulDissociated.subset

added def MulDissociated

added theorem MulEquiv.mulDissociated_preimage

added theorem mulDissociated_empty

added theorem mulDissociated_iff_sum_eq_subsingleton

added theorem mulDissociated_inv

added theorem mulDissociated_singleton

added theorem not_mulDissociated

added theorem not_mulDissociated_iff_exists_disjoint