OAI/Combinatorics/Progressions/Polynomial/PolynomialGridCover.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.inverse_power_monoline 9 - theorem
OAI.Erdos3.one_le_inverse_powerline 15 - def
OAI.Erdos3.polynomialGridCoverline 20 - theorem
OAI.Erdos3.rationalGridMajorBox_ceil_cardline 24 - theorem
OAI.Erdos3.polynomialGridCover_cardline 46