OAI/Analysis/LaughlinGap/Certificate9.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Certificate9.

  1. def OAI.LaughlinGap.RealOccupation.Certificate9.keys line 19
  2. def OAI.LaughlinGap.RealOccupation.Certificate9.fibers line 20
  3. def OAI.LaughlinGap.RealOccupation.Certificate9.columns line 21
  4. def OAI.LaughlinGap.RealOccupation.Certificate9.Y line 22
  5. def OAI.LaughlinGap.RealOccupation.Certificate9.Z line 23
  6. def OAI.LaughlinGap.RealOccupation.Certificate9.W line 24
  7. def OAI.LaughlinGap.RealOccupation.Certificate9.M line 25
  8. def OAI.LaughlinGap.RealOccupation.Certificate9.L line 26
  9. def OAI.LaughlinGap.RealOccupation.Certificate9.diag line 27
  10. def OAI.LaughlinGap.RealOccupation.Certificate9.keyIndexTable line 29
  11. def OAI.LaughlinGap.RealOccupation.Certificate9.keyIndex line 30
  12. def OAI.LaughlinGap.RealOccupation.Certificate9.representatives line 32
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_0 line 33
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_1 line 36
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_2 line 39
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_3 line 42
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_4 line 45
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_5 line 48
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_6 line 51
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_7 line 54
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_8 line 57
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover_9 line 60
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate9.cover line 63
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate9.representatives_checked line 77
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate9.keys_checked line 80
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate9.keys_injective line 83
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate9.keys_card line 84
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate9.fibers_cover line 85
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate9.fibers_sound line 90
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate9.fibers_checked line 94
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate9.columns_checked_0 line 98
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate9.columns_checked_1 line 101
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate9.columns_checked_2 line 104
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate9.columns_checked_3 line 107
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate9.columns_checked_4 line 110
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate9.columns_checked line 113
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate9.gram_checked_0 line 121
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate9.gram_checked_1 line 124
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate9.gram_checked_2 line 127
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate9.gram_checked_3 line 130
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate9.gram_checked_4 line 133
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate9.gram_checked line 136
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_table_checked_0 line 144
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_table_checked_1 line 147
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_table_checked_2 line 150
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_table_checked_3 line 153
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_table_checked_4 line 156
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_table_checked line 159
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate9.rows_checked line 167
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate9.product_checked_0 line 170
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate9.product_checked_1 line 173
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate9.product_checked_2 line 176
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate9.product_checked_3 line 179
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate9.product_checked_4 line 182
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate9.product_checked line 185
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate9.compression_checked_0 line 193
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate9.compression_checked_1 line 196
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate9.compression_checked_2 line 199
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate9.compression_checked_3 line 202
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate9.compression_checked_4 line 205
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate9.compression_checked line 208
  62. lemma OAI.LaughlinGap.RealOccupation.Certificate9.ldl_checked_0 line 216
  63. lemma OAI.LaughlinGap.RealOccupation.Certificate9.ldl_checked_1 line 219
  64. lemma OAI.LaughlinGap.RealOccupation.Certificate9.ldl_checked_2 line 222
  65. lemma OAI.LaughlinGap.RealOccupation.Certificate9.ldl_checked_3 line 225
  66. lemma OAI.LaughlinGap.RealOccupation.Certificate9.ldl_checked_4 line 228
  67. lemma OAI.LaughlinGap.RealOccupation.Certificate9.ldl_checked line 231
  68. lemma OAI.LaughlinGap.RealOccupation.Certificate9.diag_checked line 239
  69. lemma OAI.LaughlinGap.RealOccupation.Certificate9.certificate line 240