OAI/Combinatorics/Progressions/Estimates/AllocatedOriginalWholeSiteSelected.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalUnitSiteSelectedAt line 23
2. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSiteSelectedAt_unit line 184
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_original_unit_site_selected line 258
4. def OAI.Erdos3.VectorPolynomial.AllocatedOriginalWholeSiteAt line 314
5. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalUnitSiteSelectedAt_whole line 456
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_original_whole_site_selected line 500