OAI/Analysis/MutuallyUnbiased/GramAssembly/Block2Data.lean

GitHub source file

147 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_0 line 11
  2. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_1 line 13
  3. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_2 line 15
  4. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_3 line 17
  5. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_4 line 19
  6. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_5 line 21
  7. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_6 line 23
  8. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_7 line 25
  9. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_8 line 27
  10. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_9 line 29
  11. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_0_10 line 31
  12. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow0 line 33
  13. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_0 line 35
  14. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_1 line 37
  15. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_2 line 39
  16. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_3 line 41
  17. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_4 line 43
  18. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_5 line 45
  19. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_6 line 47
  20. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_7 line 49
  21. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_8 line 51
  22. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_9 line 53
  23. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_1_10 line 55
  24. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow1 line 57
  25. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_0 line 59
  26. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_1 line 61
  27. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_2 line 63
  28. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_3 line 65
  29. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_4 line 67
  30. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_5 line 69
  31. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_6 line 71
  32. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_7 line 73
  33. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_8 line 75
  34. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_9 line 77
  35. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_2_10 line 79
  36. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow2 line 81
  37. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_0 line 83
  38. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_1 line 85
  39. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_2 line 87
  40. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_3 line 89
  41. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_4 line 91
  42. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_5 line 93
  43. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_6 line 95
  44. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_7 line 97
  45. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_8 line 99
  46. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_9 line 101
  47. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_3_10 line 103
  48. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow3 line 105
  49. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_0 line 107
  50. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_1 line 109
  51. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_2 line 111
  52. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_3 line 113
  53. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_4 line 115
  54. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_5 line 117
  55. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_6 line 119
  56. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_7 line 121
  57. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_8 line 123
  58. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_9 line 125
  59. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_4_10 line 127
  60. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow4 line 129
  61. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_0 line 131
  62. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_1 line 133
  63. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_2 line 135
  64. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_3 line 137
  65. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_4 line 139
  66. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_5 line 141
  67. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_6 line 143
  68. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_7 line 145
  69. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_8 line 147
  70. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_9 line 149
  71. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_5_10 line 151
  72. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow5 line 153
  73. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_0 line 155
  74. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_1 line 157
  75. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_2 line 159
  76. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_3 line 161
  77. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_4 line 163
  78. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_5 line 165
  79. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_6 line 167
  80. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_7 line 169
  81. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_8 line 171
  82. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_9 line 173
  83. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_6_10 line 175
  84. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow6 line 177
  85. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_0 line 179
  86. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_1 line 181
  87. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_2 line 183
  88. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_3 line 185
  89. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_4 line 187
  90. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_5 line 189
  91. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_6 line 191
  92. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_7 line 193
  93. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_8 line 195
  94. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_9 line 197
  95. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_7_10 line 199
  96. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow7 line 201
  97. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_0 line 203
  98. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_1 line 205
  99. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_2 line 207
  100. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_3 line 209
  101. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_4 line 211
  102. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_5 line 213
  103. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_6 line 215
  104. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_7 line 217
  105. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_8 line 219
  106. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_9 line 221
  107. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_8_10 line 223
  108. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow8 line 225
  109. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_0 line 227
  110. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_1 line 229
  111. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_2 line 231
  112. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_3 line 233
  113. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_4 line 235
  114. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_5 line 237
  115. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_6 line 239
  116. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_7 line 241
  117. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_8 line 243
  118. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_9 line 245
  119. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_9_10 line 247
  120. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow9 line 249
  121. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_0 line 251
  122. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_1 line 253
  123. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_2 line 255
  124. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_3 line 257
  125. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_4 line 259
  126. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_5 line 261
  127. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_6 line 263
  128. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_7 line 265
  129. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_8 line 267
  130. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_9 line 269
  131. def OAI.MUB6.Certificate.GramAssembly.Block2.entry_10_10 line 271
  132. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRow10 line 273
  133. def OAI.MUB6.Certificate.GramAssembly.Block2.entryRows line 275
  134. def OAI.MUB6.Certificate.GramAssembly.Block2.entries line 277
  135. def OAI.MUB6.Certificate.GramAssembly.Block2.weights line 280
  136. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_0 line 294
  137. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_1 line 299
  138. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_2 line 304
  139. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_3 line 309
  140. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_4 line 314
  141. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_5 line 319
  142. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_6 line 324
  143. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_7 line 329
  144. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_8 line 334
  145. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_9 line 339
  146. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast_10 line 344
  147. theorem OAI.MUB6.Certificate.GramAssembly.Block2.weights_cast line 349