OAI/Combinatorics/Progressions/Polynomial/FiniteMomentPolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.finiteMomentPolynomial line 15
2. theorem OAI.Erdos3.finiteMomentPolynomial_coeff line 18
3. theorem OAI.Erdos3.finiteMomentPolynomial_ne_zero line 24
4. theorem OAI.Erdos3.finiteMomentPolynomial_natDegree_le line 33
5. theorem OAI.Erdos3.finiteMomentPolynomial_eval line 39
6. def OAI.Erdos3.momentProduct line 43
7. theorem OAI.Erdos3.momentProduct_ne_zero_some line 47