OAI/Analysis/LaughlinGap/Certificate7.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Certificate7.

  1. def OAI.LaughlinGap.RealOccupation.Certificate7.keys line 18
  2. def OAI.LaughlinGap.RealOccupation.Certificate7.fibers line 19
  3. def OAI.LaughlinGap.RealOccupation.Certificate7.columns line 20
  4. def OAI.LaughlinGap.RealOccupation.Certificate7.Y line 21
  5. def OAI.LaughlinGap.RealOccupation.Certificate7.Z line 22
  6. def OAI.LaughlinGap.RealOccupation.Certificate7.W line 23
  7. def OAI.LaughlinGap.RealOccupation.Certificate7.M line 24
  8. def OAI.LaughlinGap.RealOccupation.Certificate7.L line 25
  9. def OAI.LaughlinGap.RealOccupation.Certificate7.diag line 26
  10. def OAI.LaughlinGap.RealOccupation.Certificate7.keyIndexTable line 28
  11. def OAI.LaughlinGap.RealOccupation.Certificate7.keyIndex line 29
  12. def OAI.LaughlinGap.RealOccupation.Certificate7.representatives line 31
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_0 line 32
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_1 line 35
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_2 line 38
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_3 line 41
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_4 line 44
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_5 line 47
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_6 line 50
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover_7 line 53
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate7.cover line 56
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate7.representatives_checked line 68
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate7.keys_checked line 71
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate7.keys_injective line 74
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate7.keys_card line 75
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate7.fibers_cover line 76
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate7.fibers_sound line 81
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate7.fibers_checked line 85
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate7.columns_checked_0 line 89
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate7.columns_checked_1 line 92
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate7.columns_checked_2 line 95
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate7.columns_checked_3 line 98
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate7.columns_checked line 101
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate7.gram_checked_0 line 108
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate7.gram_checked_1 line 111
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate7.gram_checked_2 line 114
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate7.gram_checked_3 line 117
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate7.gram_checked line 120
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate7.rows_table_checked_0 line 127
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate7.rows_table_checked_1 line 130
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate7.rows_table_checked_2 line 133
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate7.rows_table_checked_3 line 136
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate7.rows_table_checked line 139
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate7.rows_checked line 146
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate7.product_checked_0 line 149
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate7.product_checked_1 line 152
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate7.product_checked_2 line 155
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate7.product_checked_3 line 158
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate7.product_checked line 161
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate7.compression_checked_0 line 168
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate7.compression_checked_1 line 171
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate7.compression_checked_2 line 174
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate7.compression_checked_3 line 177
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate7.compression_checked line 180
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate7.ldl_checked_0 line 187
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate7.ldl_checked_1 line 190
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate7.ldl_checked_2 line 193
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate7.ldl_checked_3 line 196
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate7.ldl_checked line 199
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate7.diag_checked line 206
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate7.certificate line 207