OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoDescartesY0.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_5 line 12
2. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_6 line 16
3. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_7 line 20
4. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_8 line 24
5. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_9 line 28
6. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_5 line 32
7. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_6 line 39
8. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_7 line 46
9. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_8 line 53
10. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_9 line 60
11. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_10 line 67
12. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_11 line 71
13. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_12 line 75
14. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_13 line 79
15. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_14 line 83
16. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_10 line 87
17. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_11 line 94
18. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_12 line 101
19. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_13 line 108
20. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_14 line 115
21. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_15 line 122
22. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_16 line 126
23. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_17 line 130
24. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_18 line 134
25. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_19 line 138
26. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_15 line 142
27. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_16 line 149
28. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_17 line 156
29. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_18 line 163
30. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_19 line 170
31. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_20 line 177
32. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_21 line 181
33. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_22 line 185
34. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_23 line 189
35. theorem OAI.InternalCatalan.barrierCase2AY_transform0_ratCoeff_24 line 193
36. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_20 line 197
37. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_21 line 204
38. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_22 line 211
39. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_23 line 218
40. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff_24 line 225
41. theorem OAI.InternalCatalan.barrierCase2AY_transform0_all_coeff_rat line 232
42. theorem OAI.InternalCatalan.barrierCase2AYTransform0Explicit_coeff line 265
43. theorem OAI.InternalCatalan.barrierCase2AY_transform0_eq_explicit line 294
44. theorem OAI.InternalCatalan.barrierCase2AY_transform0_signVariations line 322
45. theorem OAI.InternalCatalan.barrierCase2AY_transform0_positive_roots_le line 334