OAI/Analysis/Laughlin/FiniteFlux/GramData13.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_13_1_1 line 43
  2. theorem OAI.Laughlin.Certificate.source_error_13_1_3 line 54
  3. theorem OAI.Laughlin.Certificate.source_error_13_1_5 line 65
  4. theorem OAI.Laughlin.Certificate.source_error_13_1_7 line 76
  5. theorem OAI.Laughlin.Certificate.source_error_13_1_9 line 87
  6. theorem OAI.Laughlin.Certificate.source_error_13_1_11 line 98
  7. theorem OAI.Laughlin.Certificate.source_error_13_1_13 line 109
  8. theorem OAI.Laughlin.Certificate.source_error_13_3_3 line 120
  9. theorem OAI.Laughlin.Certificate.source_error_13_3_5 line 131
  10. theorem OAI.Laughlin.Certificate.source_error_13_3_7 line 142
  11. theorem OAI.Laughlin.Certificate.source_error_13_3_9 line 153
  12. theorem OAI.Laughlin.Certificate.source_error_13_3_11 line 164
  13. theorem OAI.Laughlin.Certificate.source_error_13_3_13 line 175
  14. theorem OAI.Laughlin.Certificate.source_error_13_5_5 line 186
  15. theorem OAI.Laughlin.Certificate.source_error_13_5_7 line 197
  16. theorem OAI.Laughlin.Certificate.source_error_13_5_9 line 208
  17. theorem OAI.Laughlin.Certificate.source_error_13_5_11 line 219
  18. theorem OAI.Laughlin.Certificate.source_error_13_5_13 line 230
  19. theorem OAI.Laughlin.Certificate.source_error_13_7_7 line 241
  20. theorem OAI.Laughlin.Certificate.source_error_13_7_9 line 252
  21. theorem OAI.Laughlin.Certificate.source_error_13_7_11 line 263
  22. theorem OAI.Laughlin.Certificate.source_error_13_7_13 line 274
  23. theorem OAI.Laughlin.Certificate.source_error_13_9_9 line 285
  24. theorem OAI.Laughlin.Certificate.source_error_13_9_11 line 296
  25. theorem OAI.Laughlin.Certificate.source_error_13_9_13 line 307
  26. theorem OAI.Laughlin.Certificate.source_error_13_11_11 line 318
  27. theorem OAI.Laughlin.Certificate.source_error_13_11_13 line 329
  28. theorem OAI.Laughlin.Certificate.source_error_13_13_13 line 340
  29. theorem OAI.Laughlin.Certificate.source_gram_13_1_1 line 351
  30. theorem OAI.Laughlin.Certificate.source_gram_13_1_3 line 355
  31. theorem OAI.Laughlin.Certificate.source_gram_13_1_5 line 359
  32. theorem OAI.Laughlin.Certificate.source_gram_13_1_7 line 363
  33. theorem OAI.Laughlin.Certificate.source_gram_13_1_9 line 367
  34. theorem OAI.Laughlin.Certificate.source_gram_13_1_11 line 371
  35. theorem OAI.Laughlin.Certificate.source_gram_13_1_13 line 375
  36. theorem OAI.Laughlin.Certificate.source_gram_13_3_3 line 379
  37. theorem OAI.Laughlin.Certificate.source_gram_13_3_5 line 383
  38. theorem OAI.Laughlin.Certificate.source_gram_13_3_7 line 387
  39. theorem OAI.Laughlin.Certificate.source_gram_13_3_9 line 391
  40. theorem OAI.Laughlin.Certificate.source_gram_13_3_11 line 395
  41. theorem OAI.Laughlin.Certificate.source_gram_13_3_13 line 399
  42. theorem OAI.Laughlin.Certificate.source_gram_13_5_5 line 403
  43. theorem OAI.Laughlin.Certificate.source_gram_13_5_7 line 407
  44. theorem OAI.Laughlin.Certificate.source_gram_13_5_9 line 411
  45. theorem OAI.Laughlin.Certificate.source_gram_13_5_11 line 415
  46. theorem OAI.Laughlin.Certificate.source_gram_13_5_13 line 419
  47. theorem OAI.Laughlin.Certificate.source_gram_13_7_7 line 423
  48. theorem OAI.Laughlin.Certificate.source_gram_13_7_9 line 427
  49. theorem OAI.Laughlin.Certificate.source_gram_13_7_11 line 431
  50. theorem OAI.Laughlin.Certificate.source_gram_13_7_13 line 435
  51. theorem OAI.Laughlin.Certificate.source_gram_13_9_9 line 439
  52. theorem OAI.Laughlin.Certificate.source_gram_13_9_11 line 443
  53. theorem OAI.Laughlin.Certificate.source_gram_13_9_13 line 447
  54. theorem OAI.Laughlin.Certificate.source_gram_13_11_11 line 451
  55. theorem OAI.Laughlin.Certificate.source_gram_13_11_13 line 455
  56. theorem OAI.Laughlin.Certificate.source_gram_13_13_13 line 459
  57. theorem OAI.Laughlin.Certificate.source_error_13_3_1 line 463
  58. theorem OAI.Laughlin.Certificate.source_gram_13_3_1 line 467
  59. theorem OAI.Laughlin.Certificate.source_error_13_5_1 line 471
  60. theorem OAI.Laughlin.Certificate.source_gram_13_5_1 line 475
  61. theorem OAI.Laughlin.Certificate.source_error_13_5_3 line 479
  62. theorem OAI.Laughlin.Certificate.source_gram_13_5_3 line 483
  63. theorem OAI.Laughlin.Certificate.source_error_13_7_1 line 487
  64. theorem OAI.Laughlin.Certificate.source_gram_13_7_1 line 491
  65. theorem OAI.Laughlin.Certificate.source_error_13_7_3 line 495
  66. theorem OAI.Laughlin.Certificate.source_gram_13_7_3 line 499
  67. theorem OAI.Laughlin.Certificate.source_error_13_7_5 line 503
  68. theorem OAI.Laughlin.Certificate.source_gram_13_7_5 line 507
  69. theorem OAI.Laughlin.Certificate.source_error_13_9_1 line 511
  70. theorem OAI.Laughlin.Certificate.source_gram_13_9_1 line 515
  71. theorem OAI.Laughlin.Certificate.source_error_13_9_3 line 519
  72. theorem OAI.Laughlin.Certificate.source_gram_13_9_3 line 523
  73. theorem OAI.Laughlin.Certificate.source_error_13_9_5 line 527
  74. theorem OAI.Laughlin.Certificate.source_gram_13_9_5 line 531
  75. theorem OAI.Laughlin.Certificate.source_error_13_9_7 line 535
  76. theorem OAI.Laughlin.Certificate.source_gram_13_9_7 line 539
  77. theorem OAI.Laughlin.Certificate.source_error_13_11_1 line 543
  78. theorem OAI.Laughlin.Certificate.source_gram_13_11_1 line 547
  79. theorem OAI.Laughlin.Certificate.source_error_13_11_3 line 551
  80. theorem OAI.Laughlin.Certificate.source_gram_13_11_3 line 555
  81. theorem OAI.Laughlin.Certificate.source_error_13_11_5 line 559
  82. theorem OAI.Laughlin.Certificate.source_gram_13_11_5 line 563
  83. theorem OAI.Laughlin.Certificate.source_error_13_11_7 line 567
  84. theorem OAI.Laughlin.Certificate.source_gram_13_11_7 line 571
  85. theorem OAI.Laughlin.Certificate.source_error_13_11_9 line 575
  86. theorem OAI.Laughlin.Certificate.source_gram_13_11_9 line 579
  87. theorem OAI.Laughlin.Certificate.source_error_13_13_1 line 583
  88. theorem OAI.Laughlin.Certificate.source_gram_13_13_1 line 587
  89. theorem OAI.Laughlin.Certificate.source_error_13_13_3 line 591
  90. theorem OAI.Laughlin.Certificate.source_gram_13_13_3 line 595
  91. theorem OAI.Laughlin.Certificate.source_error_13_13_5 line 599
  92. theorem OAI.Laughlin.Certificate.source_gram_13_13_5 line 603
  93. theorem OAI.Laughlin.Certificate.source_error_13_13_7 line 607
  94. theorem OAI.Laughlin.Certificate.source_gram_13_13_7 line 611
  95. theorem OAI.Laughlin.Certificate.source_error_13_13_9 line 615
  96. theorem OAI.Laughlin.Certificate.source_gram_13_13_9 line 619
  97. theorem OAI.Laughlin.Certificate.source_error_13_13_11 line 623
  98. theorem OAI.Laughlin.Certificate.source_gram_13_13_11 line 627
  99. theorem OAI.Laughlin.Certificate.error_13 line 631
  100. theorem OAI.Laughlin.Certificate.gram_13 line 684