OAI/Analysis/Laughlin/FiniteFlux/GramData11.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Certificate.source_error_11_1_1 line 14
  2. theorem OAI.Laughlin.Certificate.source_error_11_1_3 line 25
  3. theorem OAI.Laughlin.Certificate.source_error_11_1_5 line 36
  4. theorem OAI.Laughlin.Certificate.source_error_11_1_7 line 47
  5. theorem OAI.Laughlin.Certificate.source_error_11_1_9 line 58
  6. theorem OAI.Laughlin.Certificate.source_error_11_1_11 line 69
  7. theorem OAI.Laughlin.Certificate.source_error_11_3_3 line 80
  8. theorem OAI.Laughlin.Certificate.source_error_11_3_5 line 91
  9. theorem OAI.Laughlin.Certificate.source_error_11_3_7 line 102
  10. theorem OAI.Laughlin.Certificate.source_error_11_3_9 line 113
  11. theorem OAI.Laughlin.Certificate.source_error_11_3_11 line 124
  12. theorem OAI.Laughlin.Certificate.source_error_11_5_5 line 135
  13. theorem OAI.Laughlin.Certificate.source_error_11_5_7 line 146
  14. theorem OAI.Laughlin.Certificate.source_error_11_5_9 line 157
  15. theorem OAI.Laughlin.Certificate.source_error_11_5_11 line 168
  16. theorem OAI.Laughlin.Certificate.source_error_11_7_7 line 179
  17. theorem OAI.Laughlin.Certificate.source_error_11_7_9 line 190
  18. theorem OAI.Laughlin.Certificate.source_error_11_7_11 line 201
  19. theorem OAI.Laughlin.Certificate.source_error_11_9_9 line 212
  20. theorem OAI.Laughlin.Certificate.source_error_11_9_11 line 223
  21. theorem OAI.Laughlin.Certificate.source_error_11_11_11 line 234
  22. theorem OAI.Laughlin.Certificate.source_gram_11_1_1 line 245
  23. theorem OAI.Laughlin.Certificate.source_gram_11_1_3 line 249
  24. theorem OAI.Laughlin.Certificate.source_gram_11_1_5 line 253
  25. theorem OAI.Laughlin.Certificate.source_gram_11_1_7 line 257
  26. theorem OAI.Laughlin.Certificate.source_gram_11_1_9 line 261
  27. theorem OAI.Laughlin.Certificate.source_gram_11_1_11 line 265
  28. theorem OAI.Laughlin.Certificate.source_gram_11_3_3 line 269
  29. theorem OAI.Laughlin.Certificate.source_gram_11_3_5 line 273
  30. theorem OAI.Laughlin.Certificate.source_gram_11_3_7 line 277
  31. theorem OAI.Laughlin.Certificate.source_gram_11_3_9 line 281
  32. theorem OAI.Laughlin.Certificate.source_gram_11_3_11 line 285
  33. theorem OAI.Laughlin.Certificate.source_gram_11_5_5 line 289
  34. theorem OAI.Laughlin.Certificate.source_gram_11_5_7 line 293
  35. theorem OAI.Laughlin.Certificate.source_gram_11_5_9 line 297
  36. theorem OAI.Laughlin.Certificate.source_gram_11_5_11 line 301
  37. theorem OAI.Laughlin.Certificate.source_gram_11_7_7 line 305
  38. theorem OAI.Laughlin.Certificate.source_gram_11_7_9 line 309
  39. theorem OAI.Laughlin.Certificate.source_gram_11_7_11 line 313
  40. theorem OAI.Laughlin.Certificate.source_gram_11_9_9 line 317
  41. theorem OAI.Laughlin.Certificate.source_gram_11_9_11 line 321
  42. theorem OAI.Laughlin.Certificate.source_gram_11_11_11 line 325
  43. theorem OAI.Laughlin.Certificate.source_error_11_3_1 line 329
  44. theorem OAI.Laughlin.Certificate.source_gram_11_3_1 line 333
  45. theorem OAI.Laughlin.Certificate.source_error_11_5_1 line 337
  46. theorem OAI.Laughlin.Certificate.source_gram_11_5_1 line 341
  47. theorem OAI.Laughlin.Certificate.source_error_11_5_3 line 345
  48. theorem OAI.Laughlin.Certificate.source_gram_11_5_3 line 349
  49. theorem OAI.Laughlin.Certificate.source_error_11_7_1 line 353
  50. theorem OAI.Laughlin.Certificate.source_gram_11_7_1 line 357
  51. theorem OAI.Laughlin.Certificate.source_error_11_7_3 line 361
  52. theorem OAI.Laughlin.Certificate.source_gram_11_7_3 line 365
  53. theorem OAI.Laughlin.Certificate.source_error_11_7_5 line 369
  54. theorem OAI.Laughlin.Certificate.source_gram_11_7_5 line 373
  55. theorem OAI.Laughlin.Certificate.source_error_11_9_1 line 377
  56. theorem OAI.Laughlin.Certificate.source_gram_11_9_1 line 381
  57. theorem OAI.Laughlin.Certificate.source_error_11_9_3 line 385
  58. theorem OAI.Laughlin.Certificate.source_gram_11_9_3 line 389
  59. theorem OAI.Laughlin.Certificate.source_error_11_9_5 line 393
  60. theorem OAI.Laughlin.Certificate.source_gram_11_9_5 line 397
  61. theorem OAI.Laughlin.Certificate.source_error_11_9_7 line 401
  62. theorem OAI.Laughlin.Certificate.source_gram_11_9_7 line 405
  63. theorem OAI.Laughlin.Certificate.source_error_11_11_1 line 409
  64. theorem OAI.Laughlin.Certificate.source_gram_11_11_1 line 413
  65. theorem OAI.Laughlin.Certificate.source_error_11_11_3 line 417
  66. theorem OAI.Laughlin.Certificate.source_gram_11_11_3 line 421
  67. theorem OAI.Laughlin.Certificate.source_error_11_11_5 line 425
  68. theorem OAI.Laughlin.Certificate.source_gram_11_11_5 line 429
  69. theorem OAI.Laughlin.Certificate.source_error_11_11_7 line 433
  70. theorem OAI.Laughlin.Certificate.source_gram_11_11_7 line 437
  71. theorem OAI.Laughlin.Certificate.source_error_11_11_9 line 441
  72. theorem OAI.Laughlin.Certificate.source_gram_11_11_9 line 445
  73. theorem OAI.Laughlin.Certificate.error_11 line 449
  74. theorem OAI.Laughlin.Certificate.gram_11 line 489