Commit 2024-05-06 08:44 6b8edd9e

View on Github →

chore: Rename Salem-Spencer sets to 3AP-free sets (#12682) Salem and Spencer were neither the first to write a paper on them, nor gave the best bounds, hence the current choice of name is a bit odd (and so is the Wikipedia page). This PR renames MulSalemSpencer to ThreeGPFree and AddSalemSpencer to ThreeAPFree.

Estimated changes

deleted theorem MulSalemSpencer.image
deleted theorem MulSalemSpencer.mono
deleted theorem MulSalemSpencer.mul_left
deleted theorem MulSalemSpencer.mul_right
deleted theorem MulSalemSpencer.of_image
deleted theorem MulSalemSpencer.prod
deleted def MulSalemSpencer
added theorem ThreeGPFree.image
added theorem ThreeGPFree.mono
added theorem ThreeGPFree.mul_left
added theorem ThreeGPFree.mul_right
added theorem ThreeGPFree.of_image
added theorem ThreeGPFree.prod
added def ThreeGPFree
deleted theorem addSalemSpencer_frontier
deleted theorem addSalemSpencer_sphere
deleted theorem mulSalemSpencer_empty
deleted theorem mulSalemSpencer_insert
deleted theorem mulSalemSpencer_pair
deleted theorem mulSalemSpencer_pi
deleted theorem mulSalemSpencer_singleton
added theorem threeAPFree_frontier
added theorem threeAPFree_sphere
added theorem threeGPFree_empty
added theorem threeGPFree_insert
added theorem threeGPFree_pair
added theorem threeGPFree_pi
added theorem threeGPFree_singleton