OAI/Combinatorics/Progressions/Sampling/AllocatedClippedFullGridIdealCover.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.VectorPolynomial.allocatedClippedFullGrid_coordinate_boundsline 30 - theorem
OAI.Erdos3.VectorPolynomial.allocatedClippedFullGridPrefactor_sites_quarterline 59 - def
OAI.Erdos3.VectorPolynomial.fullGridCoverAxisDecidableEqline 125 - theorem
OAI.Erdos3.VectorPolynomial.exists_allocated_clipped_full_grid_coverline 133 - theorem
OAI.Erdos3.VectorPolynomial.exists_allocated_clipped_full_grid_ideal_coverline 239