Commit 2025-12-05 16:31 27545314

View on Github →

feat(Combinatorics/Additive): subset-sum definition and basic properties (#31689) Add subset-sum definition, basic properties and cardinality lower bound

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Created Mathlib/Combinatorics/Additive/SubsetSum.lean

added theorem Finset.card_add_card_subsetSum_lt_card_subsetSum_insert_max

added theorem Finset.card_choose_two_lt_card_subsetSum_of_nonneg

added theorem Finset.card_succ_choose_two_lt_card_subsetSum_of_pos

added theorem Finset.mem_subsetSum_iff

added theorem Finset.nonneg_of_mem_subsetSum

added def Finset.subsetSum

added theorem Finset.subsetSum_erase_zero

added theorem Finset.subsetSum_mono

added theorem Finset.subsetSum_nonempty

added theorem Finset.subset_subsetSum

added theorem Finset.vadd_finset_subsetSum_subset_subsetSum_insert

added theorem Finset.zero_mem_subsetSum

Modified Mathlib/Data/Nat/Choose/Basic.lean

Modified docs/references.bib