OAI/Combinatorics/Progressions/Estimates/CoefficientPairCover.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientTorus_continuous line 14
2. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientTorus_cover line 21
3. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbient_pair_integral_common_cover line 30
4. theorem OAI.Erdos3.VectorPolynomial.exists_finite_pair_common_cover line 56
5. theorem OAI.Erdos3.VectorPolynomial.exists_finite_pair_common_cover_with_base line 66
6. theorem OAI.Erdos3.VectorPolynomial.div_factor_of_mul_dvd line 73
7. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbient_pair_integral_divisors line 82