OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoDescartesY2Group3.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.barrierCase2AYTransform2Coefficient line 9
  2. def OAI.InternalCatalan.barrierCase2AYTransform2Explicit line 36
  3. theorem OAI.InternalCatalan.barrierCase2AYTransform2Explicit_natDegree line 63
  4. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_0 line 68
  5. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_1 line 72
  6. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_2 line 76
  7. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_3 line 80
  8. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_4 line 84
  9. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_0 line 88
  10. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_1 line 96
  11. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_2 line 104
  12. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_3 line 112
  13. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_4 line 120
  14. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_5 line 128
  15. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_6 line 132
  16. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_7 line 136
  17. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_8 line 140
  18. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_9 line 144
  19. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_5 line 148
  20. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_6 line 156
  21. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_7 line 164
  22. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_8 line 172
  23. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_9 line 180
  24. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_10 line 188
  25. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_11 line 192
  26. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_12 line 196
  27. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_13 line 200
  28. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_14 line 204
  29. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_10 line 208
  30. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_11 line 216
  31. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_12 line 224
  32. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_13 line 232
  33. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_14 line 240
  34. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_15 line 248
  35. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_16 line 252
  36. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_17 line 256
  37. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_18 line 260
  38. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_coeff_rat_19 line 264
  39. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_15 line 268
  40. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_16 line 276
  41. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_17 line 284
  42. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_18 line 292
  43. theorem OAI.InternalCatalan.barrier_case2_AY_transform2_explicit_coeff_19 line 300