OAI/Combinatorics/Progressions/Polynomial/RealBlockPolynomialEval.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.blockMonomial line 12
  2. theorem OAI.Erdos3.blockMonomial_coefficient line 17
  3. def OAI.Erdos3.factorialBlockMonomial line 26
  4. theorem OAI.Erdos3.factorialBlockMonomial_coefficient line 30
  5. def OAI.Erdos3.blockPolynomialEval line 50
  6. theorem OAI.Erdos3.blockPolynomialEval_coefficient line 55
  7. theorem OAI.Erdos3.realFactorialBlockMonomial_coefficient line 89
  8. def OAI.Erdos3.realBlockPolynomialEval line 104
  9. theorem OAI.Erdos3.realBlockPolynomialEval_coefficient line 109