Commit 2023-05-20 11:53 52ae3054

View on Github →

feat: port Combinatorics.Additive.SalemSpencer (#4128)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Additive/SalemSpencer.lean

added theorem AddSalemSpencer.le_rothNumberNat

added theorem MulSalemSpencer.image

added theorem MulSalemSpencer.le_mulRothNumber

added theorem MulSalemSpencer.mono

added theorem MulSalemSpencer.mul_left

added theorem MulSalemSpencer.mul_left₀

added theorem MulSalemSpencer.mul_right

added theorem MulSalemSpencer.mul_right₀

added theorem MulSalemSpencer.of_image

added theorem MulSalemSpencer.prod

added theorem MulSalemSpencer.roth_number_eq

added def MulSalemSpencer

added theorem Set.Subsingleton.mulSalemSpencer

added theorem addRothNumber_Ico

added theorem addSalemSpencer_frontier

added theorem addSalemSpencer_iff_eq_right

added theorem addSalemSpencer_sphere

added theorem le_mulRothNumber_product

added def mulRothNumber

added theorem mulRothNumber_empty

added theorem mulRothNumber_le

added theorem mulRothNumber_lt_of_forall_not_mulSalemSpencer

added theorem mulRothNumber_map_mul_left

added theorem mulRothNumber_map_mul_right

added theorem mulRothNumber_singleton

added theorem mulRothNumber_spec

added theorem mulRothNumber_union_le

added theorem mulSalemSpencer_empty

added theorem mulSalemSpencer_insert

added theorem mulSalemSpencer_insert_of_lt

added theorem mulSalemSpencer_mul_left_iff

added theorem mulSalemSpencer_mul_left_iff₀

added theorem mulSalemSpencer_mul_right_iff

added theorem mulSalemSpencer_mul_right_iff₀

added theorem mulSalemSpencer_pair

added theorem mulSalemSpencer_pi

added theorem mulSalemSpencer_singleton

added def rothNumberNat

added theorem rothNumberNat_add_le

added theorem rothNumberNat_def

added theorem rothNumberNat_isBigOWith_id

added theorem rothNumberNat_isBigO_id

added theorem rothNumberNat_le

added theorem rothNumberNat_spec

added theorem rothNumberNat_zero