OAI/Combinatorics/Progressions/Polynomial/DetectedTranslationBasePolynomialBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial line 18
2. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coordinate line 25
3. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coefficients_apply line 33
4. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coefficients line 42
5. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_mul line 52
6. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_factorization line 66
7. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_fast_coefficients_mem_span line 76
8. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_slow_coefficients line 112
9. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_exists_coefficient_grid line 123