OAI/Analysis/LaughlinGap/Certificate10.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Certificate10.

  1. def OAI.LaughlinGap.RealOccupation.Certificate10.keys line 17
  2. def OAI.LaughlinGap.RealOccupation.Certificate10.fibers line 18
  3. def OAI.LaughlinGap.RealOccupation.Certificate10.columns line 19
  4. def OAI.LaughlinGap.RealOccupation.Certificate10.Y line 20
  5. def OAI.LaughlinGap.RealOccupation.Certificate10.Z line 21
  6. def OAI.LaughlinGap.RealOccupation.Certificate10.W line 22
  7. def OAI.LaughlinGap.RealOccupation.Certificate10.M line 23
  8. def OAI.LaughlinGap.RealOccupation.Certificate10.L line 24
  9. def OAI.LaughlinGap.RealOccupation.Certificate10.diag line 25
  10. def OAI.LaughlinGap.RealOccupation.Certificate10.keyIndexTable line 27
  11. def OAI.LaughlinGap.RealOccupation.Certificate10.keyIndex line 28
  12. def OAI.LaughlinGap.RealOccupation.Certificate10.representatives line 30
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_0 line 31
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_1 line 34
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_2 line 37
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_3 line 40
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_4 line 43
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_5 line 46
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_6 line 49
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_7 line 52
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_8 line 55
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_9 line 58
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover_10 line 61
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate10.cover line 64
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate10.representatives_checked line 79
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate10.keys_checked line 82
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate10.keys_injective line 85
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate10.keys_card line 86
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate10.fibers_cover line 87
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate10.fibers_sound line 92
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate10.fibers_checked line 96
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate10.columns_checked_0 line 100
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate10.columns_checked_1 line 103
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate10.columns_checked_2 line 106
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate10.columns_checked_3 line 109
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate10.columns_checked_4 line 112
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate10.columns_checked line 115
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate10.gram_checked_0 line 123
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate10.gram_checked_1 line 126
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate10.gram_checked_2 line 129
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate10.gram_checked_3 line 132
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate10.gram_checked_4 line 135
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate10.gram_checked line 138
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_table_checked_0 line 146
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_table_checked_1 line 149
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_table_checked_2 line 152
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_table_checked_3 line 155
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_table_checked_4 line 158
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_table_checked line 161
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate10.rows_checked line 169
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate10.product_checked_0 line 172
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate10.product_checked_1 line 175
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate10.product_checked_2 line 178
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate10.product_checked_3 line 181
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate10.product_checked_4 line 184
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate10.product_checked line 187
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate10.compression_checked_0 line 195
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate10.compression_checked_1 line 198
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate10.compression_checked_2 line 201
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate10.compression_checked_3 line 204
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate10.compression_checked_4 line 207
  62. lemma OAI.LaughlinGap.RealOccupation.Certificate10.compression_checked line 210
  63. lemma OAI.LaughlinGap.RealOccupation.Certificate10.ldl_checked_0 line 218
  64. lemma OAI.LaughlinGap.RealOccupation.Certificate10.ldl_checked_1 line 221
  65. lemma OAI.LaughlinGap.RealOccupation.Certificate10.ldl_checked_2 line 224
  66. lemma OAI.LaughlinGap.RealOccupation.Certificate10.ldl_checked_3 line 227
  67. lemma OAI.LaughlinGap.RealOccupation.Certificate10.ldl_checked_4 line 230
  68. lemma OAI.LaughlinGap.RealOccupation.Certificate10.ldl_checked line 233
  69. lemma OAI.LaughlinGap.RealOccupation.Certificate10.diag_checked line 241
  70. lemma OAI.LaughlinGap.RealOccupation.Certificate10.certificate line 242