OAI/Analysis/Laughlin/FiniteFlux/GramData15.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_15_1_1 line 52
  2. theorem OAI.Laughlin.Certificate.source_error_15_1_3 line 63
  3. theorem OAI.Laughlin.Certificate.source_error_15_1_5 line 74
  4. theorem OAI.Laughlin.Certificate.source_error_15_1_7 line 85
  5. theorem OAI.Laughlin.Certificate.source_error_15_1_9 line 96
  6. theorem OAI.Laughlin.Certificate.source_error_15_1_11 line 107
  7. theorem OAI.Laughlin.Certificate.source_error_15_1_13 line 118
  8. theorem OAI.Laughlin.Certificate.source_error_15_1_15 line 129
  9. theorem OAI.Laughlin.Certificate.source_error_15_3_3 line 140
  10. theorem OAI.Laughlin.Certificate.source_error_15_3_5 line 151
  11. theorem OAI.Laughlin.Certificate.source_error_15_3_7 line 162
  12. theorem OAI.Laughlin.Certificate.source_error_15_3_9 line 173
  13. theorem OAI.Laughlin.Certificate.source_error_15_3_11 line 184
  14. theorem OAI.Laughlin.Certificate.source_error_15_3_13 line 195
  15. theorem OAI.Laughlin.Certificate.source_error_15_3_15 line 206
  16. theorem OAI.Laughlin.Certificate.source_error_15_5_5 line 217
  17. theorem OAI.Laughlin.Certificate.source_error_15_5_7 line 228
  18. theorem OAI.Laughlin.Certificate.source_error_15_5_9 line 239
  19. theorem OAI.Laughlin.Certificate.source_error_15_5_11 line 250
  20. theorem OAI.Laughlin.Certificate.source_error_15_5_13 line 261
  21. theorem OAI.Laughlin.Certificate.source_error_15_5_15 line 272
  22. theorem OAI.Laughlin.Certificate.source_error_15_7_7 line 283
  23. theorem OAI.Laughlin.Certificate.source_error_15_7_9 line 294
  24. theorem OAI.Laughlin.Certificate.source_error_15_7_11 line 305
  25. theorem OAI.Laughlin.Certificate.source_error_15_7_13 line 316
  26. theorem OAI.Laughlin.Certificate.source_error_15_7_15 line 327
  27. theorem OAI.Laughlin.Certificate.source_error_15_9_9 line 338
  28. theorem OAI.Laughlin.Certificate.source_error_15_9_11 line 349
  29. theorem OAI.Laughlin.Certificate.source_error_15_9_13 line 360
  30. theorem OAI.Laughlin.Certificate.source_error_15_9_15 line 371
  31. theorem OAI.Laughlin.Certificate.source_error_15_11_11 line 382
  32. theorem OAI.Laughlin.Certificate.source_error_15_11_13 line 393
  33. theorem OAI.Laughlin.Certificate.source_error_15_11_15 line 404
  34. theorem OAI.Laughlin.Certificate.source_error_15_13_13 line 415
  35. theorem OAI.Laughlin.Certificate.source_error_15_13_15 line 426
  36. theorem OAI.Laughlin.Certificate.source_error_15_15_15 line 437
  37. theorem OAI.Laughlin.Certificate.source_gram_15_1_1 line 448
  38. theorem OAI.Laughlin.Certificate.source_gram_15_1_3 line 452
  39. theorem OAI.Laughlin.Certificate.source_gram_15_1_5 line 456
  40. theorem OAI.Laughlin.Certificate.source_gram_15_1_7 line 460
  41. theorem OAI.Laughlin.Certificate.source_gram_15_1_9 line 464
  42. theorem OAI.Laughlin.Certificate.source_gram_15_1_11 line 468
  43. theorem OAI.Laughlin.Certificate.source_gram_15_1_13 line 472
  44. theorem OAI.Laughlin.Certificate.source_gram_15_1_15 line 476
  45. theorem OAI.Laughlin.Certificate.source_gram_15_3_3 line 480
  46. theorem OAI.Laughlin.Certificate.source_gram_15_3_5 line 484
  47. theorem OAI.Laughlin.Certificate.source_gram_15_3_7 line 488
  48. theorem OAI.Laughlin.Certificate.source_gram_15_3_9 line 492
  49. theorem OAI.Laughlin.Certificate.source_gram_15_3_11 line 496
  50. theorem OAI.Laughlin.Certificate.source_gram_15_3_13 line 500
  51. theorem OAI.Laughlin.Certificate.source_gram_15_3_15 line 504
  52. theorem OAI.Laughlin.Certificate.source_gram_15_5_5 line 508
  53. theorem OAI.Laughlin.Certificate.source_gram_15_5_7 line 512
  54. theorem OAI.Laughlin.Certificate.source_gram_15_5_9 line 516
  55. theorem OAI.Laughlin.Certificate.source_gram_15_5_11 line 520
  56. theorem OAI.Laughlin.Certificate.source_gram_15_5_13 line 524
  57. theorem OAI.Laughlin.Certificate.source_gram_15_5_15 line 528
  58. theorem OAI.Laughlin.Certificate.source_gram_15_7_7 line 532
  59. theorem OAI.Laughlin.Certificate.source_gram_15_7_9 line 536
  60. theorem OAI.Laughlin.Certificate.source_gram_15_7_11 line 540
  61. theorem OAI.Laughlin.Certificate.source_gram_15_7_13 line 544
  62. theorem OAI.Laughlin.Certificate.source_gram_15_7_15 line 548
  63. theorem OAI.Laughlin.Certificate.source_gram_15_9_9 line 552
  64. theorem OAI.Laughlin.Certificate.source_gram_15_9_11 line 556
  65. theorem OAI.Laughlin.Certificate.source_gram_15_9_13 line 560
  66. theorem OAI.Laughlin.Certificate.source_gram_15_9_15 line 564
  67. theorem OAI.Laughlin.Certificate.source_gram_15_11_11 line 568
  68. theorem OAI.Laughlin.Certificate.source_gram_15_11_13 line 572
  69. theorem OAI.Laughlin.Certificate.source_gram_15_11_15 line 576
  70. theorem OAI.Laughlin.Certificate.source_gram_15_13_13 line 580
  71. theorem OAI.Laughlin.Certificate.source_gram_15_13_15 line 584
  72. theorem OAI.Laughlin.Certificate.source_gram_15_15_15 line 588
  73. theorem OAI.Laughlin.Certificate.source_error_15_3_1 line 592
  74. theorem OAI.Laughlin.Certificate.source_gram_15_3_1 line 596
  75. theorem OAI.Laughlin.Certificate.source_error_15_5_1 line 600
  76. theorem OAI.Laughlin.Certificate.source_gram_15_5_1 line 604
  77. theorem OAI.Laughlin.Certificate.source_error_15_5_3 line 608
  78. theorem OAI.Laughlin.Certificate.source_gram_15_5_3 line 612
  79. theorem OAI.Laughlin.Certificate.source_error_15_7_1 line 616
  80. theorem OAI.Laughlin.Certificate.source_gram_15_7_1 line 620
  81. theorem OAI.Laughlin.Certificate.source_error_15_7_3 line 624
  82. theorem OAI.Laughlin.Certificate.source_gram_15_7_3 line 628
  83. theorem OAI.Laughlin.Certificate.source_error_15_7_5 line 632
  84. theorem OAI.Laughlin.Certificate.source_gram_15_7_5 line 636
  85. theorem OAI.Laughlin.Certificate.source_error_15_9_1 line 640
  86. theorem OAI.Laughlin.Certificate.source_gram_15_9_1 line 644
  87. theorem OAI.Laughlin.Certificate.source_error_15_9_3 line 648
  88. theorem OAI.Laughlin.Certificate.source_gram_15_9_3 line 652
  89. theorem OAI.Laughlin.Certificate.source_error_15_9_5 line 656
  90. theorem OAI.Laughlin.Certificate.source_gram_15_9_5 line 660
  91. theorem OAI.Laughlin.Certificate.source_error_15_9_7 line 664
  92. theorem OAI.Laughlin.Certificate.source_gram_15_9_7 line 668
  93. theorem OAI.Laughlin.Certificate.source_error_15_11_1 line 672
  94. theorem OAI.Laughlin.Certificate.source_gram_15_11_1 line 676
  95. theorem OAI.Laughlin.Certificate.source_error_15_11_3 line 680
  96. theorem OAI.Laughlin.Certificate.source_gram_15_11_3 line 684
  97. theorem OAI.Laughlin.Certificate.source_error_15_11_5 line 688
  98. theorem OAI.Laughlin.Certificate.source_gram_15_11_5 line 692
  99. theorem OAI.Laughlin.Certificate.source_error_15_11_7 line 696
  100. theorem OAI.Laughlin.Certificate.source_gram_15_11_7 line 700
  101. theorem OAI.Laughlin.Certificate.source_error_15_11_9 line 704
  102. theorem OAI.Laughlin.Certificate.source_gram_15_11_9 line 708
  103. theorem OAI.Laughlin.Certificate.source_error_15_13_1 line 712
  104. theorem OAI.Laughlin.Certificate.source_gram_15_13_1 line 716
  105. theorem OAI.Laughlin.Certificate.source_error_15_13_3 line 720
  106. theorem OAI.Laughlin.Certificate.source_gram_15_13_3 line 724
  107. theorem OAI.Laughlin.Certificate.source_error_15_13_5 line 728
  108. theorem OAI.Laughlin.Certificate.source_gram_15_13_5 line 732
  109. theorem OAI.Laughlin.Certificate.source_error_15_13_7 line 736
  110. theorem OAI.Laughlin.Certificate.source_gram_15_13_7 line 740
  111. theorem OAI.Laughlin.Certificate.source_error_15_13_9 line 744
  112. theorem OAI.Laughlin.Certificate.source_gram_15_13_9 line 748
  113. theorem OAI.Laughlin.Certificate.source_error_15_13_11 line 752
  114. theorem OAI.Laughlin.Certificate.source_gram_15_13_11 line 756
  115. theorem OAI.Laughlin.Certificate.source_error_15_15_1 line 760
  116. theorem OAI.Laughlin.Certificate.source_gram_15_15_1 line 764
  117. theorem OAI.Laughlin.Certificate.source_error_15_15_3 line 768
  118. theorem OAI.Laughlin.Certificate.source_gram_15_15_3 line 772
  119. theorem OAI.Laughlin.Certificate.source_error_15_15_5 line 776
  120. theorem OAI.Laughlin.Certificate.source_gram_15_15_5 line 780
  121. theorem OAI.Laughlin.Certificate.source_error_15_15_7 line 784
  122. theorem OAI.Laughlin.Certificate.source_gram_15_15_7 line 788
  123. theorem OAI.Laughlin.Certificate.source_error_15_15_9 line 792
  124. theorem OAI.Laughlin.Certificate.source_gram_15_15_9 line 796
  125. theorem OAI.Laughlin.Certificate.source_error_15_15_11 line 800
  126. theorem OAI.Laughlin.Certificate.source_gram_15_15_11 line 804
  127. theorem OAI.Laughlin.Certificate.source_error_15_15_13 line 808
  128. theorem OAI.Laughlin.Certificate.source_gram_15_15_13 line 812
  129. theorem OAI.Laughlin.Certificate.error_15 line 816
  130. theorem OAI.Laughlin.Certificate.gram_15 line 884