Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 15:33 108eb0b2

View on Github →

feat(combinatorics/additive/salem_spencer): Salem-Spencer sets and Roth numbers (#10509) This defines Salem-Spencer sets and Roth numbers in (additive) monoids.

Estimated changes

added theorem add_roth_number_Ico
added def mul_roth_number
added theorem mul_roth_number_empty
added theorem mul_roth_number_le
added theorem mul_roth_number_spec
added theorem mul_salem_spencer.mono
added theorem mul_salem_spencer.prod
added theorem mul_salem_spencer_pair
added theorem mul_salem_spencer_pi
added def roth_number_nat
added theorem roth_number_nat_add_le
added theorem roth_number_nat_def
added theorem roth_number_nat_le
added theorem roth_number_nat_spec
added theorem roth_number_nat_zero
added theorem finset.preimage_subset
added theorem finset.subset_map_iff