OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoDescartesY0Group0.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrierCase2AY_coeff_0 line 10
  2. theorem OAI.InternalCatalan.barrierCase2AY_coeff_1 line 17
  3. theorem OAI.InternalCatalan.barrierCase2AY_coeff_2 line 24
  4. theorem OAI.InternalCatalan.barrierCase2AY_coeff_3 line 31
  5. theorem OAI.InternalCatalan.barrierCase2AY_coeff_4 line 38
  6. theorem OAI.InternalCatalan.barrierCase2AY_coeff_5 line 45
  7. theorem OAI.InternalCatalan.barrierCase2AY_coeff_6 line 52
  8. theorem OAI.InternalCatalan.barrierCase2AY_coeff_7 line 59
  9. theorem OAI.InternalCatalan.barrierCase2AY_coeff_8 line 66
  10. theorem OAI.InternalCatalan.barrierCase2AY_coeff_9 line 73
  11. theorem OAI.InternalCatalan.barrierCase2AY_coeff_10 line 80
  12. theorem OAI.InternalCatalan.barrierCase2AY_coeff_11 line 87
  13. theorem OAI.InternalCatalan.barrierCase2AY_coeff_12 line 94
  14. theorem OAI.InternalCatalan.barrierCase2AY_coeff_13 line 101
  15. theorem OAI.InternalCatalan.barrierCase2AY_coeff_14 line 108
  16. theorem OAI.InternalCatalan.barrierCase2AY_coeff_15 line 115
  17. theorem OAI.InternalCatalan.barrierCase2AY_coeff_16 line 122
  18. theorem OAI.InternalCatalan.barrierCase2AY_coeff_17 line 129
  19. theorem OAI.InternalCatalan.barrierCase2AY_coeff_18 line 136
  20. theorem OAI.InternalCatalan.barrierCase2AY_coeff_19 line 143
  21. theorem OAI.InternalCatalan.barrierCase2AY_coeff_20 line 150
  22. theorem OAI.InternalCatalan.barrierCase2AY_coeff_21 line 157
  23. theorem OAI.InternalCatalan.barrierCase2AY_coeff_22 line 164
  24. theorem OAI.InternalCatalan.barrierCase2AY_coeff_23 line 171
  25. theorem OAI.InternalCatalan.barrierCase2AY_coeff_24 line 178
  26. theorem OAI.InternalCatalan.barrierCase2AY_coeff_small line 187
  27. def OAI.InternalCatalan.barrierCase2AYTransform0Coefficient line 218
  28. def OAI.InternalCatalan.barrierCase2AYTransform0Explicit line 245
  29. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_natDegree line 272
  30. def OAI.InternalCatalan.barrierCase2AYTransform1Coefficient line 279
  31. def OAI.InternalCatalan.barrierCase2AYTransform1Explicit line 306
  32. theorem OAI.InternalCatalan.barrierCase2AYTransform1Explicit_natDegree line 333
  33. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_0 line 338
  34. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_1 line 342
  35. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_2 line 346
  36. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_3 line 350
  37. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_4 line 354
  38. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_0 line 358
  39. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_1 line 365
  40. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_2 line 372
  41. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_3 line 379
  42. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_4 line 386