OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoDescartesX0.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_15 line 11
2. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_15 line 15
3. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_16 line 22
4. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_16 line 26
5. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_17 line 33
6. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_17 line 37
7. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_18 line 44
8. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_18 line 48
9. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_19 line 55
10. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_19 line 59
11. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_20 line 66
12. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_20 line 70
13. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_21 line 77
14. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_21 line 81
15. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_22 line 88
16. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_22 line 92
17. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_23 line 99
18. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_23 line 103
19. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_24 line 110
20. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_24 line 114
21. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_25 line 121
22. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_25 line 125
23. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_26 line 132
24. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_26 line 136
25. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_27 line 143
26. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_27 line 147
27. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_28 line 154
28. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_28 line 158
29. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_29 line 165
30. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_29 line 169
31. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_30 line 176
32. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_30 line 180
33. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_31 line 187
34. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_31 line 191
35. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_32 line 198
36. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_32 line 202
37. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_33 line 209
38. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_33 line 213
39. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_34 line 220
40. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_34 line 224
41. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_35 line 231
42. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_35 line 235
43. theorem OAI.InternalCatalan.barrierCase2AX_transform0_ratCoeff_36 line 242
44. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff_36 line 246
45. theorem OAI.InternalCatalan.barrierCase2AX_transform0_all_coeff_rat line 253
46. theorem OAI.InternalCatalan.barrierCase2AXTransform0Explicit_coeff line 298
47. theorem OAI.InternalCatalan.barrierCase2AX_transform0_eq_explicit line 339
48. theorem OAI.InternalCatalan.barrierCase2AX_transform0_signVariations line 361
49. theorem OAI.InternalCatalan.barrierCase2AX_transform0_positive_roots_le line 373