OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoXRootSimplicity.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_15 line 18
2. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_15 line 22
3. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_16 line 29
4. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_16 line 33
5. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_17 line 40
6. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_17 line 44
7. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_18 line 51
8. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_18 line 55
9. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_19 line 62
10. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_19 line 66
11. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_20 line 73
12. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_20 line 77
13. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_21 line 84
14. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_21 line 88
15. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_22 line 95
16. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_22 line 99
17. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_23 line 106
18. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_23 line 110
19. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_24 line 117
20. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_24 line 121
21. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_25 line 128
22. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_25 line 132
23. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_26 line 139
24. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_26 line 143
25. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_27 line 150
26. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_27 line 154
27. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_28 line 161
28. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_28 line 165
29. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_29 line 172
30. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_29 line 176
31. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_30 line 183
32. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_30 line 187
33. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_31 line 194
34. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_31 line 198
35. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_32 line 205
36. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_32 line 209
37. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_33 line 216
38. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_33 line 220
39. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_34 line 227
40. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_34 line 231
41. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_35 line 238
42. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_35 line 242
43. theorem OAI.InternalCatalan.barrierCase2AX_transform1_ratCoeff_36 line 249
44. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff_36 line 253
45. theorem OAI.InternalCatalan.barrierCase2AX_transform1_all_coeff_rat line 260
46. theorem OAI.InternalCatalan.barrierCase2AXTransform1Explicit_coeff line 305
47. theorem OAI.InternalCatalan.barrierCase2AX_transform1_eq_explicit line 346
48. theorem OAI.InternalCatalan.barrierCase2AX_transform1_signVariations line 368
49. theorem OAI.InternalCatalan.barrierCase2AX_transform1_positive_roots_le line 380
50. theorem OAI.InternalCatalan.barrierCase2AX_mapped_natDegree_le line 387
51. theorem OAI.InternalCatalan.barrierCase2AX_interval0_roots_card_le line 393
52. theorem OAI.InternalCatalan.barrierCase2AX_interval1_roots_card_le line 407
53. theorem OAI.InternalCatalan.barrierCase2AX_domain_roots_card_le line 421
54. theorem OAI.InternalCatalan.barrierCase2X_bracket_subset_domain line 448
55. theorem OAI.InternalCatalan.barrierCase2X_brackets_disjoint line 461
56. def OAI.InternalCatalan.barrierCase2XChosenRoot line 485
57. theorem OAI.InternalCatalan.barrierCase2XChosenRoot_spec line 490
58. def OAI.InternalCatalan.barrierCase2XChosenRoots line 498
59. theorem OAI.InternalCatalan.barrierCase2XChosenRoots_card line 502
60. theorem OAI.InternalCatalan.barrierCase2XChosenRoots_spec line 517
61. theorem OAI.InternalCatalan.barrierCase2AX_root_mem_chosen line 528
62. theorem OAI.InternalCatalan.barrierCase2AX_roots_exhausted line 543
63. def OAI.InternalCatalan.case2XSimplicityNegativeBrackets line 555
64. def OAI.InternalCatalan.case2XSimplicityPositiveBrackets line 560
65. theorem OAI.InternalCatalan.case2XSimplicity_degree_le line 565
66. theorem OAI.InternalCatalan.case2XSimplicity_negative line 571
67. theorem OAI.InternalCatalan.case2XSimplicity_positive line 604
68. theorem OAI.InternalCatalan.barrierCase2AX_rootMultiplicity_eq_one line 637
69. theorem OAI.InternalCatalan.barrierCase2AX_derivative_ne_zero_at_root line 645
70. theorem OAI.InternalCatalan.case2XSimplicity_bracket_subset_domain line 659
71. theorem OAI.InternalCatalan.case2XSimplicity_brackets_disjoint line 672
72. def OAI.InternalCatalan.case2XSimplicityChosenRoot line 696
73. theorem OAI.InternalCatalan.case2XSimplicityChosenRoot_spec line 701
74. def OAI.InternalCatalan.case2XSimplicityChosenRoots line 709
75. theorem OAI.InternalCatalan.case2XSimplicityChosenRoots_card line 713
76. theorem OAI.InternalCatalan.case2XSimplicityChosenRoots_spec line 728
77. theorem OAI.InternalCatalan.case2XSimplicity_root_mem_chosen line 739
78. theorem OAI.InternalCatalan.barrierCase2AX_unique_root_in_bracket line 754
79. theorem OAI.InternalCatalan.barrierCase2AX_simple_root_in_bracket line 772
80. theorem OAI.InternalCatalan.barrierCase2AX_unique_simple_root_in_bracket line 781