Commit 2024-05-07 09:25 859845f1

View on Github →

refactor: Redefine 3AP-free sets (#12701) The current definition allows {0, 1} as a 3AP-free set in ZMod 2, which is really inconvenient from the point of view of interfacing with corners. This PR redefines it so that 0, 1, 0 in ZMod 2 is a 3AP and {0, 1} is not 3AP-free. Also take the opportunity to reorder the binders to a more convenient fashion, to move the heavy result threeAPFree_sphere to Combinatorics.Additive.Behrend where it is used (it won't be used anywhere else) and to drop rothNumberNat_isBigO_id since it's a trivial result that pulls in a bunch of analysis.

Estimated changes

Modified Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

added theorem threeAPFree_frontier

added theorem threeAPFree_sphere

Modified Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

added theorem ThreeGPFree.eq_right

added theorem ThreeGPFree.mulRothNumber_eq

deleted theorem ThreeGPFree.mul_left

deleted theorem ThreeGPFree.mul_left₀

deleted theorem ThreeGPFree.mul_right

deleted theorem ThreeGPFree.mul_right₀

deleted theorem ThreeGPFree.roth_number_eq

added theorem ThreeGPFree.smul_set

added theorem ThreeGPFree.smul_set₀

modified def ThreeGPFree

deleted theorem rothNumberNat_isBigOWith_id

deleted theorem rothNumberNat_isBigO_id

deleted theorem threeAPFree_frontier

deleted theorem threeAPFree_sphere

modified theorem threeGPFree_insert

deleted theorem threeGPFree_mul_left_iff

deleted theorem threeGPFree_mul_left_iff₀

deleted theorem threeGPFree_mul_right_iff

deleted theorem threeGPFree_mul_right_iff₀

deleted theorem threeGPFree_pair

added theorem threeGPFree_smul_set

added theorem threeGPFree_smul_set₀