OAI/Analysis/Laughlin/FiniteFlux/GramData17.lean

GitHub source file

164 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_17_1_1 line 62
  2. theorem OAI.Laughlin.Certificate.source_error_17_1_3 line 73
  3. theorem OAI.Laughlin.Certificate.source_error_17_1_5 line 84
  4. theorem OAI.Laughlin.Certificate.source_error_17_1_7 line 95
  5. theorem OAI.Laughlin.Certificate.source_error_17_1_9 line 106
  6. theorem OAI.Laughlin.Certificate.source_error_17_1_11 line 117
  7. theorem OAI.Laughlin.Certificate.source_error_17_1_13 line 128
  8. theorem OAI.Laughlin.Certificate.source_error_17_1_15 line 139
  9. theorem OAI.Laughlin.Certificate.source_error_17_1_17 line 150
  10. theorem OAI.Laughlin.Certificate.source_error_17_3_3 line 161
  11. theorem OAI.Laughlin.Certificate.source_error_17_3_5 line 172
  12. theorem OAI.Laughlin.Certificate.source_error_17_3_7 line 183
  13. theorem OAI.Laughlin.Certificate.source_error_17_3_9 line 194
  14. theorem OAI.Laughlin.Certificate.source_error_17_3_11 line 205
  15. theorem OAI.Laughlin.Certificate.source_error_17_3_13 line 216
  16. theorem OAI.Laughlin.Certificate.source_error_17_3_15 line 227
  17. theorem OAI.Laughlin.Certificate.source_error_17_3_17 line 238
  18. theorem OAI.Laughlin.Certificate.source_error_17_5_5 line 249
  19. theorem OAI.Laughlin.Certificate.source_error_17_5_7 line 260
  20. theorem OAI.Laughlin.Certificate.source_error_17_5_9 line 271
  21. theorem OAI.Laughlin.Certificate.source_error_17_5_11 line 282
  22. theorem OAI.Laughlin.Certificate.source_error_17_5_13 line 293
  23. theorem OAI.Laughlin.Certificate.source_error_17_5_15 line 304
  24. theorem OAI.Laughlin.Certificate.source_error_17_5_17 line 315
  25. theorem OAI.Laughlin.Certificate.source_error_17_7_7 line 326
  26. theorem OAI.Laughlin.Certificate.source_error_17_7_9 line 337
  27. theorem OAI.Laughlin.Certificate.source_error_17_7_11 line 348
  28. theorem OAI.Laughlin.Certificate.source_error_17_7_13 line 359
  29. theorem OAI.Laughlin.Certificate.source_error_17_7_15 line 370
  30. theorem OAI.Laughlin.Certificate.source_error_17_7_17 line 381
  31. theorem OAI.Laughlin.Certificate.source_error_17_9_9 line 392
  32. theorem OAI.Laughlin.Certificate.source_error_17_9_11 line 403
  33. theorem OAI.Laughlin.Certificate.source_error_17_9_13 line 414
  34. theorem OAI.Laughlin.Certificate.source_error_17_9_15 line 425
  35. theorem OAI.Laughlin.Certificate.source_error_17_9_17 line 436
  36. theorem OAI.Laughlin.Certificate.source_error_17_11_11 line 447
  37. theorem OAI.Laughlin.Certificate.source_error_17_11_13 line 458
  38. theorem OAI.Laughlin.Certificate.source_error_17_11_15 line 469
  39. theorem OAI.Laughlin.Certificate.source_error_17_11_17 line 480
  40. theorem OAI.Laughlin.Certificate.source_error_17_13_13 line 491
  41. theorem OAI.Laughlin.Certificate.source_error_17_13_15 line 502
  42. theorem OAI.Laughlin.Certificate.source_error_17_13_17 line 513
  43. theorem OAI.Laughlin.Certificate.source_error_17_15_15 line 524
  44. theorem OAI.Laughlin.Certificate.source_error_17_15_17 line 535
  45. theorem OAI.Laughlin.Certificate.source_error_17_17_17 line 546
  46. theorem OAI.Laughlin.Certificate.source_gram_17_1_1 line 557
  47. theorem OAI.Laughlin.Certificate.source_gram_17_1_3 line 561
  48. theorem OAI.Laughlin.Certificate.source_gram_17_1_5 line 565
  49. theorem OAI.Laughlin.Certificate.source_gram_17_1_7 line 569
  50. theorem OAI.Laughlin.Certificate.source_gram_17_1_9 line 573
  51. theorem OAI.Laughlin.Certificate.source_gram_17_1_11 line 577
  52. theorem OAI.Laughlin.Certificate.source_gram_17_1_13 line 581
  53. theorem OAI.Laughlin.Certificate.source_gram_17_1_15 line 585
  54. theorem OAI.Laughlin.Certificate.source_gram_17_1_17 line 589
  55. theorem OAI.Laughlin.Certificate.source_gram_17_3_3 line 593
  56. theorem OAI.Laughlin.Certificate.source_gram_17_3_5 line 597
  57. theorem OAI.Laughlin.Certificate.source_gram_17_3_7 line 601
  58. theorem OAI.Laughlin.Certificate.source_gram_17_3_9 line 605
  59. theorem OAI.Laughlin.Certificate.source_gram_17_3_11 line 609
  60. theorem OAI.Laughlin.Certificate.source_gram_17_3_13 line 613
  61. theorem OAI.Laughlin.Certificate.source_gram_17_3_15 line 617
  62. theorem OAI.Laughlin.Certificate.source_gram_17_3_17 line 621
  63. theorem OAI.Laughlin.Certificate.source_gram_17_5_5 line 625
  64. theorem OAI.Laughlin.Certificate.source_gram_17_5_7 line 629
  65. theorem OAI.Laughlin.Certificate.source_gram_17_5_9 line 633
  66. theorem OAI.Laughlin.Certificate.source_gram_17_5_11 line 637
  67. theorem OAI.Laughlin.Certificate.source_gram_17_5_13 line 641
  68. theorem OAI.Laughlin.Certificate.source_gram_17_5_15 line 645
  69. theorem OAI.Laughlin.Certificate.source_gram_17_5_17 line 649
  70. theorem OAI.Laughlin.Certificate.source_gram_17_7_7 line 653
  71. theorem OAI.Laughlin.Certificate.source_gram_17_7_9 line 657
  72. theorem OAI.Laughlin.Certificate.source_gram_17_7_11 line 661
  73. theorem OAI.Laughlin.Certificate.source_gram_17_7_13 line 665
  74. theorem OAI.Laughlin.Certificate.source_gram_17_7_15 line 669
  75. theorem OAI.Laughlin.Certificate.source_gram_17_7_17 line 673
  76. theorem OAI.Laughlin.Certificate.source_gram_17_9_9 line 677
  77. theorem OAI.Laughlin.Certificate.source_gram_17_9_11 line 681
  78. theorem OAI.Laughlin.Certificate.source_gram_17_9_13 line 685
  79. theorem OAI.Laughlin.Certificate.source_gram_17_9_15 line 689
  80. theorem OAI.Laughlin.Certificate.source_gram_17_9_17 line 693
  81. theorem OAI.Laughlin.Certificate.source_gram_17_11_11 line 697
  82. theorem OAI.Laughlin.Certificate.source_gram_17_11_13 line 701
  83. theorem OAI.Laughlin.Certificate.source_gram_17_11_15 line 705
  84. theorem OAI.Laughlin.Certificate.source_gram_17_11_17 line 709
  85. theorem OAI.Laughlin.Certificate.source_gram_17_13_13 line 713
  86. theorem OAI.Laughlin.Certificate.source_gram_17_13_15 line 717
  87. theorem OAI.Laughlin.Certificate.source_gram_17_13_17 line 721
  88. theorem OAI.Laughlin.Certificate.source_gram_17_15_15 line 725
  89. theorem OAI.Laughlin.Certificate.source_gram_17_15_17 line 729
  90. theorem OAI.Laughlin.Certificate.source_gram_17_17_17 line 733
  91. theorem OAI.Laughlin.Certificate.source_error_17_3_1 line 737
  92. theorem OAI.Laughlin.Certificate.source_gram_17_3_1 line 741
  93. theorem OAI.Laughlin.Certificate.source_error_17_5_1 line 745
  94. theorem OAI.Laughlin.Certificate.source_gram_17_5_1 line 749
  95. theorem OAI.Laughlin.Certificate.source_error_17_5_3 line 753
  96. theorem OAI.Laughlin.Certificate.source_gram_17_5_3 line 757
  97. theorem OAI.Laughlin.Certificate.source_error_17_7_1 line 761
  98. theorem OAI.Laughlin.Certificate.source_gram_17_7_1 line 765
  99. theorem OAI.Laughlin.Certificate.source_error_17_7_3 line 769
  100. theorem OAI.Laughlin.Certificate.source_gram_17_7_3 line 773
  101. theorem OAI.Laughlin.Certificate.source_error_17_7_5 line 777
  102. theorem OAI.Laughlin.Certificate.source_gram_17_7_5 line 781
  103. theorem OAI.Laughlin.Certificate.source_error_17_9_1 line 785
  104. theorem OAI.Laughlin.Certificate.source_gram_17_9_1 line 789
  105. theorem OAI.Laughlin.Certificate.source_error_17_9_3 line 793
  106. theorem OAI.Laughlin.Certificate.source_gram_17_9_3 line 797
  107. theorem OAI.Laughlin.Certificate.source_error_17_9_5 line 801
  108. theorem OAI.Laughlin.Certificate.source_gram_17_9_5 line 805
  109. theorem OAI.Laughlin.Certificate.source_error_17_9_7 line 809
  110. theorem OAI.Laughlin.Certificate.source_gram_17_9_7 line 813
  111. theorem OAI.Laughlin.Certificate.source_error_17_11_1 line 817
  112. theorem OAI.Laughlin.Certificate.source_gram_17_11_1 line 821
  113. theorem OAI.Laughlin.Certificate.source_error_17_11_3 line 825
  114. theorem OAI.Laughlin.Certificate.source_gram_17_11_3 line 829
  115. theorem OAI.Laughlin.Certificate.source_error_17_11_5 line 833
  116. theorem OAI.Laughlin.Certificate.source_gram_17_11_5 line 837
  117. theorem OAI.Laughlin.Certificate.source_error_17_11_7 line 841
  118. theorem OAI.Laughlin.Certificate.source_gram_17_11_7 line 845
  119. theorem OAI.Laughlin.Certificate.source_error_17_11_9 line 849
  120. theorem OAI.Laughlin.Certificate.source_gram_17_11_9 line 853
  121. theorem OAI.Laughlin.Certificate.source_error_17_13_1 line 857
  122. theorem OAI.Laughlin.Certificate.source_gram_17_13_1 line 861
  123. theorem OAI.Laughlin.Certificate.source_error_17_13_3 line 865
  124. theorem OAI.Laughlin.Certificate.source_gram_17_13_3 line 869
  125. theorem OAI.Laughlin.Certificate.source_error_17_13_5 line 873
  126. theorem OAI.Laughlin.Certificate.source_gram_17_13_5 line 877
  127. theorem OAI.Laughlin.Certificate.source_error_17_13_7 line 881
  128. theorem OAI.Laughlin.Certificate.source_gram_17_13_7 line 885
  129. theorem OAI.Laughlin.Certificate.source_error_17_13_9 line 889
  130. theorem OAI.Laughlin.Certificate.source_gram_17_13_9 line 893
  131. theorem OAI.Laughlin.Certificate.source_error_17_13_11 line 897
  132. theorem OAI.Laughlin.Certificate.source_gram_17_13_11 line 901
  133. theorem OAI.Laughlin.Certificate.source_error_17_15_1 line 905
  134. theorem OAI.Laughlin.Certificate.source_gram_17_15_1 line 909
  135. theorem OAI.Laughlin.Certificate.source_error_17_15_3 line 913
  136. theorem OAI.Laughlin.Certificate.source_gram_17_15_3 line 917
  137. theorem OAI.Laughlin.Certificate.source_error_17_15_5 line 921
  138. theorem OAI.Laughlin.Certificate.source_gram_17_15_5 line 925
  139. theorem OAI.Laughlin.Certificate.source_error_17_15_7 line 929
  140. theorem OAI.Laughlin.Certificate.source_gram_17_15_7 line 933
  141. theorem OAI.Laughlin.Certificate.source_error_17_15_9 line 937
  142. theorem OAI.Laughlin.Certificate.source_gram_17_15_9 line 941
  143. theorem OAI.Laughlin.Certificate.source_error_17_15_11 line 945
  144. theorem OAI.Laughlin.Certificate.source_gram_17_15_11 line 949
  145. theorem OAI.Laughlin.Certificate.source_error_17_15_13 line 953
  146. theorem OAI.Laughlin.Certificate.source_gram_17_15_13 line 957
  147. theorem OAI.Laughlin.Certificate.source_error_17_17_1 line 961
  148. theorem OAI.Laughlin.Certificate.source_gram_17_17_1 line 965
  149. theorem OAI.Laughlin.Certificate.source_error_17_17_3 line 969
  150. theorem OAI.Laughlin.Certificate.source_gram_17_17_3 line 973
  151. theorem OAI.Laughlin.Certificate.source_error_17_17_5 line 977
  152. theorem OAI.Laughlin.Certificate.source_gram_17_17_5 line 981
  153. theorem OAI.Laughlin.Certificate.source_error_17_17_7 line 985
  154. theorem OAI.Laughlin.Certificate.source_gram_17_17_7 line 989
  155. theorem OAI.Laughlin.Certificate.source_error_17_17_9 line 993
  156. theorem OAI.Laughlin.Certificate.source_gram_17_17_9 line 997
  157. theorem OAI.Laughlin.Certificate.source_error_17_17_11 line 1001
  158. theorem OAI.Laughlin.Certificate.source_gram_17_17_11 line 1005
  159. theorem OAI.Laughlin.Certificate.source_error_17_17_13 line 1009
  160. theorem OAI.Laughlin.Certificate.source_gram_17_17_13 line 1013
  161. theorem OAI.Laughlin.Certificate.source_error_17_17_15 line 1017
  162. theorem OAI.Laughlin.Certificate.source_gram_17_17_15 line 1021
  163. theorem OAI.Laughlin.Certificate.error_17 line 1025
  164. theorem OAI.Laughlin.Certificate.gram_17 line 1110