OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXTailCoefficientsP.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2PTailNumeratorCoefficient line 13
  2. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_0 line 25
  3. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_1 line 31
  4. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_2 line 37
  5. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_3 line 43
  6. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_4 line 49
  7. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_5 line 55
  8. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_6 line 61
  9. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_7 line 67
  10. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_8 line 73
  11. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff_9 line 79
  12. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_natDegree line 85
  13. theorem OAI.InternalCatalan.barrierCase2PTailNumeratorExplicit_coeff line 90
  14. def OAI.InternalCatalan.barrierCase2PTailProductCoefficient line 113
  15. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_0 line 126
  16. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_1 line 132
  17. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_2 line 138
  18. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_3 line 144
  19. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_4 line 150
  20. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_5 line 156
  21. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_6 line 162
  22. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_7 line 168
  23. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_8 line 174
  24. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_9 line 180
  25. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff_10 line 186
  26. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_natDegree line 192
  27. theorem OAI.InternalCatalan.barrierCase2PTailProductExplicit_coeff line 197