OAI/Analysis/MutuallyUnbiased/GramAssembly/Combined.lean

GitHub source file

184 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.combined0part0 line 12
  2. def OAI.MUB6.Certificate.GramAssembly.combined0part1 line 14
  3. def OAI.MUB6.Certificate.GramAssembly.combined0part2 line 16
  4. def OAI.MUB6.Certificate.GramAssembly.combined0part3 line 18
  5. def OAI.MUB6.Certificate.GramAssembly.combined0part4 line 20
  6. def OAI.MUB6.Certificate.GramAssembly.combined0part5 line 22
  7. def OAI.MUB6.Certificate.GramAssembly.combined0part6 line 24
  8. def OAI.MUB6.Certificate.GramAssembly.combined0part7 line 26
  9. def OAI.MUB6.Certificate.GramAssembly.combined0part8 line 28
  10. def OAI.MUB6.Certificate.GramAssembly.combined0part9 line 30
  11. def OAI.MUB6.Certificate.GramAssembly.combined0part10 line 32
  12. def OAI.MUB6.Certificate.GramAssembly.combined0part11 line 34
  13. def OAI.MUB6.Certificate.GramAssembly.combined0part12 line 36
  14. def OAI.MUB6.Certificate.GramAssembly.combined0part13 line 38
  15. def OAI.MUB6.Certificate.GramAssembly.combined0part14 line 40
  16. def OAI.MUB6.Certificate.GramAssembly.combined0part15 line 42
  17. def OAI.MUB6.Certificate.GramAssembly.combined0part16 line 44
  18. def OAI.MUB6.Certificate.GramAssembly.combined0part17 line 46
  19. def OAI.MUB6.Certificate.GramAssembly.combined0part18 line 48
  20. def OAI.MUB6.Certificate.GramAssembly.combined0part19 line 50
  21. def OAI.MUB6.Certificate.GramAssembly.combined0part20 line 52
  22. def OAI.MUB6.Certificate.GramAssembly.combined0part21 line 54
  23. def OAI.MUB6.Certificate.GramAssembly.combined0part22 line 56
  24. def OAI.MUB6.Certificate.GramAssembly.combined0part23 line 58
  25. def OAI.MUB6.Certificate.GramAssembly.combined0part24 line 60
  26. def OAI.MUB6.Certificate.GramAssembly.combined0part25 line 62
  27. def OAI.MUB6.Certificate.GramAssembly.combined0part26 line 64
  28. def OAI.MUB6.Certificate.GramAssembly.combined0part27 line 66
  29. def OAI.MUB6.Certificate.GramAssembly.combined0 line 68
  30. theorem OAI.MUB6.Certificate.GramAssembly.combined0_check line 70
  31. theorem OAI.MUB6.Certificate.GramAssembly.combined0_eval line 73
  32. def OAI.MUB6.Certificate.GramAssembly.combined1part0 line 78
  33. def OAI.MUB6.Certificate.GramAssembly.combined1part1 line 80
  34. def OAI.MUB6.Certificate.GramAssembly.combined1part2 line 82
  35. def OAI.MUB6.Certificate.GramAssembly.combined1part3 line 84
  36. def OAI.MUB6.Certificate.GramAssembly.combined1part4 line 86
  37. def OAI.MUB6.Certificate.GramAssembly.combined1part5 line 88
  38. def OAI.MUB6.Certificate.GramAssembly.combined1part6 line 90
  39. def OAI.MUB6.Certificate.GramAssembly.combined1part7 line 92
  40. def OAI.MUB6.Certificate.GramAssembly.combined1part8 line 94
  41. def OAI.MUB6.Certificate.GramAssembly.combined1part9 line 96
  42. def OAI.MUB6.Certificate.GramAssembly.combined1part10 line 98
  43. def OAI.MUB6.Certificate.GramAssembly.combined1part11 line 100
  44. def OAI.MUB6.Certificate.GramAssembly.combined1part12 line 102
  45. def OAI.MUB6.Certificate.GramAssembly.combined1part13 line 104
  46. def OAI.MUB6.Certificate.GramAssembly.combined1part14 line 106
  47. def OAI.MUB6.Certificate.GramAssembly.combined1part15 line 108
  48. def OAI.MUB6.Certificate.GramAssembly.combined1part16 line 110
  49. def OAI.MUB6.Certificate.GramAssembly.combined1part17 line 112
  50. def OAI.MUB6.Certificate.GramAssembly.combined1part18 line 114
  51. def OAI.MUB6.Certificate.GramAssembly.combined1part19 line 116
  52. def OAI.MUB6.Certificate.GramAssembly.combined1part20 line 118
  53. def OAI.MUB6.Certificate.GramAssembly.combined1part21 line 120
  54. def OAI.MUB6.Certificate.GramAssembly.combined1part22 line 122
  55. def OAI.MUB6.Certificate.GramAssembly.combined1part23 line 124
  56. def OAI.MUB6.Certificate.GramAssembly.combined1part24 line 126
  57. def OAI.MUB6.Certificate.GramAssembly.combined1part25 line 128
  58. def OAI.MUB6.Certificate.GramAssembly.combined1part26 line 130
  59. def OAI.MUB6.Certificate.GramAssembly.combined1part27 line 132
  60. def OAI.MUB6.Certificate.GramAssembly.combined1part28 line 134
  61. def OAI.MUB6.Certificate.GramAssembly.combined1part29 line 136
  62. def OAI.MUB6.Certificate.GramAssembly.combined1 line 138
  63. theorem OAI.MUB6.Certificate.GramAssembly.combined1_check line 140
  64. theorem OAI.MUB6.Certificate.GramAssembly.combined1_eval line 143
  65. def OAI.MUB6.Certificate.GramAssembly.combined2part0 line 149
  66. def OAI.MUB6.Certificate.GramAssembly.combined2part1 line 151
  67. def OAI.MUB6.Certificate.GramAssembly.combined2part2 line 153
  68. def OAI.MUB6.Certificate.GramAssembly.combined2part3 line 155
  69. def OAI.MUB6.Certificate.GramAssembly.combined2part4 line 157
  70. def OAI.MUB6.Certificate.GramAssembly.combined2part5 line 159
  71. def OAI.MUB6.Certificate.GramAssembly.combined2part6 line 161
  72. def OAI.MUB6.Certificate.GramAssembly.combined2part7 line 163
  73. def OAI.MUB6.Certificate.GramAssembly.combined2part8 line 165
  74. def OAI.MUB6.Certificate.GramAssembly.combined2part9 line 167
  75. def OAI.MUB6.Certificate.GramAssembly.combined2part10 line 169
  76. def OAI.MUB6.Certificate.GramAssembly.combined2part11 line 171
  77. def OAI.MUB6.Certificate.GramAssembly.combined2part12 line 173
  78. def OAI.MUB6.Certificate.GramAssembly.combined2part13 line 175
  79. def OAI.MUB6.Certificate.GramAssembly.combined2part14 line 177
  80. def OAI.MUB6.Certificate.GramAssembly.combined2part15 line 179
  81. def OAI.MUB6.Certificate.GramAssembly.combined2part16 line 181
  82. def OAI.MUB6.Certificate.GramAssembly.combined2part17 line 183
  83. def OAI.MUB6.Certificate.GramAssembly.combined2part18 line 185
  84. def OAI.MUB6.Certificate.GramAssembly.combined2part19 line 187
  85. def OAI.MUB6.Certificate.GramAssembly.combined2part20 line 189
  86. def OAI.MUB6.Certificate.GramAssembly.combined2part21 line 191
  87. def OAI.MUB6.Certificate.GramAssembly.combined2part22 line 193
  88. def OAI.MUB6.Certificate.GramAssembly.combined2part23 line 195
  89. def OAI.MUB6.Certificate.GramAssembly.combined2part24 line 197
  90. def OAI.MUB6.Certificate.GramAssembly.combined2part25 line 199
  91. def OAI.MUB6.Certificate.GramAssembly.combined2part26 line 201
  92. def OAI.MUB6.Certificate.GramAssembly.combined2part27 line 203
  93. def OAI.MUB6.Certificate.GramAssembly.combined2 line 205
  94. theorem OAI.MUB6.Certificate.GramAssembly.combined2_check line 207
  95. theorem OAI.MUB6.Certificate.GramAssembly.combined2_eval line 210
  96. def OAI.MUB6.Certificate.GramAssembly.combined3part0 line 215
  97. def OAI.MUB6.Certificate.GramAssembly.combined3part1 line 217
  98. def OAI.MUB6.Certificate.GramAssembly.combined3part2 line 219
  99. def OAI.MUB6.Certificate.GramAssembly.combined3part3 line 221
  100. def OAI.MUB6.Certificate.GramAssembly.combined3part4 line 223
  101. def OAI.MUB6.Certificate.GramAssembly.combined3part5 line 225
  102. def OAI.MUB6.Certificate.GramAssembly.combined3part6 line 227
  103. def OAI.MUB6.Certificate.GramAssembly.combined3part7 line 229
  104. def OAI.MUB6.Certificate.GramAssembly.combined3part8 line 231
  105. def OAI.MUB6.Certificate.GramAssembly.combined3part9 line 233
  106. def OAI.MUB6.Certificate.GramAssembly.combined3part10 line 235
  107. def OAI.MUB6.Certificate.GramAssembly.combined3part11 line 237
  108. def OAI.MUB6.Certificate.GramAssembly.combined3part12 line 239
  109. def OAI.MUB6.Certificate.GramAssembly.combined3part13 line 241
  110. def OAI.MUB6.Certificate.GramAssembly.combined3part14 line 243
  111. def OAI.MUB6.Certificate.GramAssembly.combined3part15 line 245
  112. def OAI.MUB6.Certificate.GramAssembly.combined3part16 line 247
  113. def OAI.MUB6.Certificate.GramAssembly.combined3part17 line 249
  114. def OAI.MUB6.Certificate.GramAssembly.combined3part18 line 251
  115. def OAI.MUB6.Certificate.GramAssembly.combined3part19 line 253
  116. def OAI.MUB6.Certificate.GramAssembly.combined3part20 line 255
  117. def OAI.MUB6.Certificate.GramAssembly.combined3part21 line 257
  118. def OAI.MUB6.Certificate.GramAssembly.combined3part22 line 259
  119. def OAI.MUB6.Certificate.GramAssembly.combined3part23 line 261
  120. def OAI.MUB6.Certificate.GramAssembly.combined3part24 line 263
  121. def OAI.MUB6.Certificate.GramAssembly.combined3part25 line 265
  122. def OAI.MUB6.Certificate.GramAssembly.combined3part26 line 267
  123. def OAI.MUB6.Certificate.GramAssembly.combined3part27 line 269
  124. def OAI.MUB6.Certificate.GramAssembly.combined3part28 line 271
  125. def OAI.MUB6.Certificate.GramAssembly.combined3part29 line 273
  126. def OAI.MUB6.Certificate.GramAssembly.combined3part30 line 275
  127. def OAI.MUB6.Certificate.GramAssembly.combined3part31 line 277
  128. def OAI.MUB6.Certificate.GramAssembly.combined3part32 line 279
  129. def OAI.MUB6.Certificate.GramAssembly.combined3part33 line 281
  130. def OAI.MUB6.Certificate.GramAssembly.combined3part34 line 283
  131. def OAI.MUB6.Certificate.GramAssembly.combined3part35 line 285
  132. def OAI.MUB6.Certificate.GramAssembly.combined3 line 287
  133. theorem OAI.MUB6.Certificate.GramAssembly.combined3_check line 289
  134. theorem OAI.MUB6.Certificate.GramAssembly.combined3_eval line 292
  135. def OAI.MUB6.Certificate.GramAssembly.combined4part0 line 298
  136. def OAI.MUB6.Certificate.GramAssembly.combined4part1 line 300
  137. def OAI.MUB6.Certificate.GramAssembly.combined4part2 line 302
  138. def OAI.MUB6.Certificate.GramAssembly.combined4part3 line 304
  139. def OAI.MUB6.Certificate.GramAssembly.combined4part4 line 306
  140. def OAI.MUB6.Certificate.GramAssembly.combined4part5 line 308
  141. def OAI.MUB6.Certificate.GramAssembly.combined4part6 line 310
  142. def OAI.MUB6.Certificate.GramAssembly.combined4part7 line 312
  143. def OAI.MUB6.Certificate.GramAssembly.combined4part8 line 314
  144. def OAI.MUB6.Certificate.GramAssembly.combined4part9 line 316
  145. def OAI.MUB6.Certificate.GramAssembly.combined4part10 line 318
  146. def OAI.MUB6.Certificate.GramAssembly.combined4part11 line 320
  147. def OAI.MUB6.Certificate.GramAssembly.combined4part12 line 322
  148. def OAI.MUB6.Certificate.GramAssembly.combined4part13 line 324
  149. def OAI.MUB6.Certificate.GramAssembly.combined4part14 line 326
  150. def OAI.MUB6.Certificate.GramAssembly.combined4part15 line 328
  151. def OAI.MUB6.Certificate.GramAssembly.combined4part16 line 330
  152. def OAI.MUB6.Certificate.GramAssembly.combined4part17 line 332
  153. def OAI.MUB6.Certificate.GramAssembly.combined4part18 line 334
  154. def OAI.MUB6.Certificate.GramAssembly.combined4part19 line 336
  155. def OAI.MUB6.Certificate.GramAssembly.combined4part20 line 338
  156. def OAI.MUB6.Certificate.GramAssembly.combined4part21 line 340
  157. def OAI.MUB6.Certificate.GramAssembly.combined4part22 line 342
  158. def OAI.MUB6.Certificate.GramAssembly.combined4part23 line 344
  159. def OAI.MUB6.Certificate.GramAssembly.combined4part24 line 346
  160. def OAI.MUB6.Certificate.GramAssembly.combined4part25 line 348
  161. def OAI.MUB6.Certificate.GramAssembly.combined4part26 line 350
  162. def OAI.MUB6.Certificate.GramAssembly.combined4part27 line 352
  163. def OAI.MUB6.Certificate.GramAssembly.combined4part28 line 354
  164. def OAI.MUB6.Certificate.GramAssembly.combined4part29 line 356
  165. def OAI.MUB6.Certificate.GramAssembly.combined4part30 line 358
  166. def OAI.MUB6.Certificate.GramAssembly.combined4part31 line 360
  167. def OAI.MUB6.Certificate.GramAssembly.combined4part32 line 362
  168. def OAI.MUB6.Certificate.GramAssembly.combined4part33 line 364
  169. def OAI.MUB6.Certificate.GramAssembly.combined4part34 line 366
  170. def OAI.MUB6.Certificate.GramAssembly.combined4part35 line 368
  171. def OAI.MUB6.Certificate.GramAssembly.combined4part36 line 370
  172. def OAI.MUB6.Certificate.GramAssembly.combined4part37 line 372
  173. def OAI.MUB6.Certificate.GramAssembly.combined4part38 line 374
  174. def OAI.MUB6.Certificate.GramAssembly.combined4part39 line 376
  175. def OAI.MUB6.Certificate.GramAssembly.combined4part40 line 378
  176. def OAI.MUB6.Certificate.GramAssembly.combined4part41 line 380
  177. def OAI.MUB6.Certificate.GramAssembly.combined4part42 line 382
  178. def OAI.MUB6.Certificate.GramAssembly.combined4part43 line 384
  179. def OAI.MUB6.Certificate.GramAssembly.combined4part44 line 386
  180. def OAI.MUB6.Certificate.GramAssembly.combined4part45 line 388
  181. def OAI.MUB6.Certificate.GramAssembly.combined4 line 390
  182. theorem OAI.MUB6.Certificate.GramAssembly.combined4_check line 392
  183. theorem OAI.MUB6.Certificate.GramAssembly.combined4_eval line 395
  184. def OAI.MUB6.Certificate.GramAssembly.polynomial line 400