OAI/Analysis/Laughlin/FiniteFlux/GramData12.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_12_1_1 line 35
  2. theorem OAI.Laughlin.Certificate.source_error_12_1_3 line 46
  3. theorem OAI.Laughlin.Certificate.source_error_12_1_5 line 57
  4. theorem OAI.Laughlin.Certificate.source_error_12_1_7 line 68
  5. theorem OAI.Laughlin.Certificate.source_error_12_1_9 line 79
  6. theorem OAI.Laughlin.Certificate.source_error_12_1_11 line 90
  7. theorem OAI.Laughlin.Certificate.source_error_12_3_3 line 101
  8. theorem OAI.Laughlin.Certificate.source_error_12_3_5 line 112
  9. theorem OAI.Laughlin.Certificate.source_error_12_3_7 line 123
  10. theorem OAI.Laughlin.Certificate.source_error_12_3_9 line 134
  11. theorem OAI.Laughlin.Certificate.source_error_12_3_11 line 145
  12. theorem OAI.Laughlin.Certificate.source_error_12_5_5 line 156
  13. theorem OAI.Laughlin.Certificate.source_error_12_5_7 line 167
  14. theorem OAI.Laughlin.Certificate.source_error_12_5_9 line 178
  15. theorem OAI.Laughlin.Certificate.source_error_12_5_11 line 189
  16. theorem OAI.Laughlin.Certificate.source_error_12_7_7 line 200
  17. theorem OAI.Laughlin.Certificate.source_error_12_7_9 line 211
  18. theorem OAI.Laughlin.Certificate.source_error_12_7_11 line 222
  19. theorem OAI.Laughlin.Certificate.source_error_12_9_9 line 233
  20. theorem OAI.Laughlin.Certificate.source_error_12_9_11 line 244
  21. theorem OAI.Laughlin.Certificate.source_error_12_11_11 line 255
  22. theorem OAI.Laughlin.Certificate.source_gram_12_1_1 line 266
  23. theorem OAI.Laughlin.Certificate.source_gram_12_1_3 line 270
  24. theorem OAI.Laughlin.Certificate.source_gram_12_1_5 line 274
  25. theorem OAI.Laughlin.Certificate.source_gram_12_1_7 line 278
  26. theorem OAI.Laughlin.Certificate.source_gram_12_1_9 line 282
  27. theorem OAI.Laughlin.Certificate.source_gram_12_1_11 line 286
  28. theorem OAI.Laughlin.Certificate.source_gram_12_3_3 line 290
  29. theorem OAI.Laughlin.Certificate.source_gram_12_3_5 line 294
  30. theorem OAI.Laughlin.Certificate.source_gram_12_3_7 line 298
  31. theorem OAI.Laughlin.Certificate.source_gram_12_3_9 line 302
  32. theorem OAI.Laughlin.Certificate.source_gram_12_3_11 line 306
  33. theorem OAI.Laughlin.Certificate.source_gram_12_5_5 line 310
  34. theorem OAI.Laughlin.Certificate.source_gram_12_5_7 line 314
  35. theorem OAI.Laughlin.Certificate.source_gram_12_5_9 line 318
  36. theorem OAI.Laughlin.Certificate.source_gram_12_5_11 line 322
  37. theorem OAI.Laughlin.Certificate.source_gram_12_7_7 line 326
  38. theorem OAI.Laughlin.Certificate.source_gram_12_7_9 line 330
  39. theorem OAI.Laughlin.Certificate.source_gram_12_7_11 line 334
  40. theorem OAI.Laughlin.Certificate.source_gram_12_9_9 line 338
  41. theorem OAI.Laughlin.Certificate.source_gram_12_9_11 line 342
  42. theorem OAI.Laughlin.Certificate.source_gram_12_11_11 line 346
  43. theorem OAI.Laughlin.Certificate.source_error_12_3_1 line 350
  44. theorem OAI.Laughlin.Certificate.source_gram_12_3_1 line 354
  45. theorem OAI.Laughlin.Certificate.source_error_12_5_1 line 358
  46. theorem OAI.Laughlin.Certificate.source_gram_12_5_1 line 362
  47. theorem OAI.Laughlin.Certificate.source_error_12_5_3 line 366
  48. theorem OAI.Laughlin.Certificate.source_gram_12_5_3 line 370
  49. theorem OAI.Laughlin.Certificate.source_error_12_7_1 line 374
  50. theorem OAI.Laughlin.Certificate.source_gram_12_7_1 line 378
  51. theorem OAI.Laughlin.Certificate.source_error_12_7_3 line 382
  52. theorem OAI.Laughlin.Certificate.source_gram_12_7_3 line 386
  53. theorem OAI.Laughlin.Certificate.source_error_12_7_5 line 390
  54. theorem OAI.Laughlin.Certificate.source_gram_12_7_5 line 394
  55. theorem OAI.Laughlin.Certificate.source_error_12_9_1 line 398
  56. theorem OAI.Laughlin.Certificate.source_gram_12_9_1 line 402
  57. theorem OAI.Laughlin.Certificate.source_error_12_9_3 line 406
  58. theorem OAI.Laughlin.Certificate.source_gram_12_9_3 line 410
  59. theorem OAI.Laughlin.Certificate.source_error_12_9_5 line 414
  60. theorem OAI.Laughlin.Certificate.source_gram_12_9_5 line 418
  61. theorem OAI.Laughlin.Certificate.source_error_12_9_7 line 422
  62. theorem OAI.Laughlin.Certificate.source_gram_12_9_7 line 426
  63. theorem OAI.Laughlin.Certificate.source_error_12_11_1 line 430
  64. theorem OAI.Laughlin.Certificate.source_gram_12_11_1 line 434
  65. theorem OAI.Laughlin.Certificate.source_error_12_11_3 line 438
  66. theorem OAI.Laughlin.Certificate.source_gram_12_11_3 line 442
  67. theorem OAI.Laughlin.Certificate.source_error_12_11_5 line 446
  68. theorem OAI.Laughlin.Certificate.source_gram_12_11_5 line 450
  69. theorem OAI.Laughlin.Certificate.source_error_12_11_7 line 454
  70. theorem OAI.Laughlin.Certificate.source_gram_12_11_7 line 458
  71. theorem OAI.Laughlin.Certificate.source_error_12_11_9 line 462
  72. theorem OAI.Laughlin.Certificate.source_gram_12_11_9 line 466
  73. theorem OAI.Laughlin.Certificate.error_12 line 470
  74. theorem OAI.Laughlin.Certificate.gram_12 line 510