OAI/Combinatorics/Progressions/Polynomial/SingleParameterPolynomial.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.fwdDiff_iter_eq_zero_of_local line 14
  2. theorem OAI.Erdos3.finite_interval_newton_formula line 26
  3. def OAI.Erdos3.integerNewtonPolynomial line 47
  4. theorem OAI.Erdos3.integerNewtonPolynomial_natDegree_le line 51
  5. theorem OAI.Erdos3.integerNewtonPolynomial_eval_nat line 59
  6. theorem OAI.Erdos3.integerNewtonPolynomial_integer_valued line 69
  7. theorem OAI.Erdos3.exists_integer_polynomial_of_local_differences line 73
  8. theorem OAI.Erdos3.exists_integer_polynomial_lift line 84
  9. theorem OAI.Erdos3.singleParameter_natDegree_le line 111
  10. theorem OAI.Erdos3.singleParameter_symm_degree line 123
  11. theorem OAI.Erdos3.singleParameter_eval line 135
  12. theorem OAI.Erdos3.singleParameter_symm_eval line 139
  13. theorem OAI.Erdos3.exists_singleParameter_integer_lift line 143