OAI/Analysis/LaughlinGap/Certificate15.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

Certificate15.

  1. def OAI.LaughlinGap.RealOccupation.Certificate15.keys line 19
  2. def OAI.LaughlinGap.RealOccupation.Certificate15.fibers line 20
  3. def OAI.LaughlinGap.RealOccupation.Certificate15.columns line 21
  4. def OAI.LaughlinGap.RealOccupation.Certificate15.Y line 22
  5. def OAI.LaughlinGap.RealOccupation.Certificate15.Z line 23
  6. def OAI.LaughlinGap.RealOccupation.Certificate15.W line 24
  7. def OAI.LaughlinGap.RealOccupation.Certificate15.M line 25
  8. def OAI.LaughlinGap.RealOccupation.Certificate15.L line 26
  9. def OAI.LaughlinGap.RealOccupation.Certificate15.diag line 27
  10. def OAI.LaughlinGap.RealOccupation.Certificate15.keyIndexTable line 29
  11. def OAI.LaughlinGap.RealOccupation.Certificate15.keyIndex line 30
  12. def OAI.LaughlinGap.RealOccupation.Certificate15.representatives line 32
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_0 line 33
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_1 line 36
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_2 line 39
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_3 line 42
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_4 line 45
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_5 line 48
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_6 line 51
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_7 line 54
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_8 line 57
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_9 line 60
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_10 line 63
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_11 line 66
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_12 line 69
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_13 line 72
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_14 line 75
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover_15 line 78
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate15.cover line 81
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate15.representatives_checked line 101
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate15.keys_checked line 104
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate15.keys_injective line 107
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate15.keys_card line 108
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate15.fibers_cover line 109
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate15.fibers_sound line 114
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate15.fibers_checked line 118
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_0 line 122
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_1 line 125
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_2 line 128
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_3 line 131
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_4 line 134
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_5 line 137
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_6 line 140
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked_7 line 143
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate15.columns_checked line 146
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_0 line 157
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_1 line 160
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_2 line 163
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_3 line 166
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_4 line 169
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_5 line 172
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_6 line 175
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked_7 line 178
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate15.gram_checked line 181
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_0 line 192
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_1 line 195
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_2 line 198
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_3 line 201
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_4 line 204
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_5 line 207
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_6 line 210
  62. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked_7 line 213
  63. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_table_checked line 216
  64. lemma OAI.LaughlinGap.RealOccupation.Certificate15.rows_checked line 227
  65. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_0 line 230
  66. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_1 line 233
  67. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_2 line 236
  68. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_3 line 239
  69. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_4 line 242
  70. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_5 line 245
  71. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_6 line 248
  72. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked_7 line 251
  73. lemma OAI.LaughlinGap.RealOccupation.Certificate15.product_checked line 254
  74. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_0 line 265
  75. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_1 line 268
  76. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_2 line 271
  77. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_3 line 274
  78. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_4 line 277
  79. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_5 line 280
  80. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_6 line 283
  81. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked_7 line 286
  82. lemma OAI.LaughlinGap.RealOccupation.Certificate15.compression_checked line 289
  83. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_0 line 300
  84. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_1 line 303
  85. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_2 line 306
  86. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_3 line 309
  87. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_4 line 312
  88. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_5 line 315
  89. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_6 line 318
  90. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked_7 line 321
  91. lemma OAI.LaughlinGap.RealOccupation.Certificate15.ldl_checked line 324
  92. lemma OAI.LaughlinGap.RealOccupation.Certificate15.diag_checked line 335
  93. lemma OAI.LaughlinGap.RealOccupation.Certificate15.certificate line 336