OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXBaseProductCoefficientsData.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit line 14
  2. def OAI.InternalCatalan.barrierCase2VTailProductExplicit line 29
  3. theorem OAI.InternalCatalan.barrierCase2VTailNumerator_eq_explicit line 45
  4. theorem OAI.InternalCatalan.barrierCase2VTailProduct_eq_explicit line 57
  5. def OAI.InternalCatalan.barrierCase2VTailNumeratorCoefficient line 69
  6. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_00 line 84
  7. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_01 line 90
  8. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_02 line 96
  9. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_03 line 102
  10. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_04 line 108
  11. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_05 line 114
  12. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_06 line 120
  13. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_07 line 126
  14. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_08 line 132
  15. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_09 line 138
  16. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_10 line 144
  17. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_11 line 150
  18. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff_12 line 156
  19. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_natDegree line 162
  20. theorem OAI.InternalCatalan.barrierCase2VTailNumeratorExplicit_coeff line 167
  21. def OAI.InternalCatalan.barrierCase2VTailProductCoefficient line 194
  22. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_00 line 210
  23. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_01 line 216
  24. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_02 line 222
  25. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_03 line 228
  26. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_04 line 234
  27. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_05 line 240
  28. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_06 line 246
  29. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_07 line 252
  30. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_08 line 258
  31. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_09 line 264
  32. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_10 line 270
  33. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_11 line 276
  34. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_12 line 282
  35. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff_13 line 288
  36. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_natDegree line 294
  37. theorem OAI.InternalCatalan.barrierCase2VTailProductExplicit_coeff line 299
  38. def OAI.InternalCatalan.barrierCase2XBaseFractions line 327
  39. def OAI.InternalCatalan.barrierCase2XBaseNumeratorExplicit line 332
  40. def OAI.InternalCatalan.barrierCase2XBaseProductExplicit line 348
  41. theorem OAI.InternalCatalan.barrier_case2_U_3 line 355

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:490 (same declaration text).

  42. theorem OAI.InternalCatalan.barrier_case2_U_4 line 359

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:494 (same declaration text).

  43. theorem OAI.InternalCatalan.barrier_case2_U_5 line 363

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:498 (same declaration text).

  44. theorem OAI.InternalCatalan.barrier_case2_U_6 line 367

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:502 (same declaration text).

  45. theorem OAI.InternalCatalan.barrier_case2_U_7 line 371

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:506 (same declaration text).

  46. theorem OAI.InternalCatalan.barrier_case2_U_8 line 375

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:510 (same declaration text).

  47. theorem OAI.InternalCatalan.barrier_case2_U_9 line 379

    Also declared: OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXExplicitGroup7.lean:514 (same declaration text).

  48. theorem OAI.InternalCatalan.barrierCase2XBaseNumerator_eq_explicit line 383
  49. theorem OAI.InternalCatalan.barrierCase2XBaseProduct_eq_explicit line 397
  50. theorem OAI.InternalCatalan.barrierCase2AX_eq_factored line 406
  51. def OAI.InternalCatalan.barrierCase2XBaseNumeratorCoefficient line 429
  52. def OAI.InternalCatalan.barrierCase2XBaseProductCoefficient line 432