OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge54.lean

GitHub source file

184 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined432_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined432_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined432_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined432_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined432_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined432_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined432_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined432_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined432_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined432_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined432_part10 line 28
  12. def OAI.MUB6.TaoCertificate.combined432_part11 line 30
  13. def OAI.MUB6.TaoCertificate.combined432_part12 line 32
  14. def OAI.MUB6.TaoCertificate.combined432_part13 line 34
  15. def OAI.MUB6.TaoCertificate.combined432_part14 line 36
  16. def OAI.MUB6.TaoCertificate.combined432_part15 line 38
  17. def OAI.MUB6.TaoCertificate.combined432_part16 line 40
  18. def OAI.MUB6.TaoCertificate.combined432_part17 line 42
  19. def OAI.MUB6.TaoCertificate.combined432_part18 line 44
  20. def OAI.MUB6.TaoCertificate.combined432_part19 line 46
  21. def OAI.MUB6.TaoCertificate.combined432 line 48
  22. theorem OAI.MUB6.TaoCertificate.combined432_checked line 50
  23. theorem OAI.MUB6.TaoCertificate.combined432_zero line 53
  24. def OAI.MUB6.TaoCertificate.combined433_part0 line 61
  25. def OAI.MUB6.TaoCertificate.combined433_part1 line 63
  26. def OAI.MUB6.TaoCertificate.combined433_part2 line 65
  27. def OAI.MUB6.TaoCertificate.combined433_part3 line 67
  28. def OAI.MUB6.TaoCertificate.combined433_part4 line 69
  29. def OAI.MUB6.TaoCertificate.combined433_part5 line 71
  30. def OAI.MUB6.TaoCertificate.combined433_part6 line 73
  31. def OAI.MUB6.TaoCertificate.combined433_part7 line 75
  32. def OAI.MUB6.TaoCertificate.combined433_part8 line 77
  33. def OAI.MUB6.TaoCertificate.combined433_part9 line 79
  34. def OAI.MUB6.TaoCertificate.combined433_part10 line 81
  35. def OAI.MUB6.TaoCertificate.combined433_part11 line 83
  36. def OAI.MUB6.TaoCertificate.combined433_part12 line 85
  37. def OAI.MUB6.TaoCertificate.combined433_part13 line 87
  38. def OAI.MUB6.TaoCertificate.combined433_part14 line 89
  39. def OAI.MUB6.TaoCertificate.combined433_part15 line 91
  40. def OAI.MUB6.TaoCertificate.combined433_part16 line 93
  41. def OAI.MUB6.TaoCertificate.combined433_part17 line 95
  42. def OAI.MUB6.TaoCertificate.combined433_part18 line 97
  43. def OAI.MUB6.TaoCertificate.combined433_part19 line 99
  44. def OAI.MUB6.TaoCertificate.combined433 line 101
  45. theorem OAI.MUB6.TaoCertificate.combined433_checked line 103
  46. theorem OAI.MUB6.TaoCertificate.combined433_zero line 106
  47. def OAI.MUB6.TaoCertificate.combined434_part0 line 114
  48. def OAI.MUB6.TaoCertificate.combined434_part1 line 116
  49. def OAI.MUB6.TaoCertificate.combined434_part2 line 118
  50. def OAI.MUB6.TaoCertificate.combined434_part3 line 120
  51. def OAI.MUB6.TaoCertificate.combined434_part4 line 122
  52. def OAI.MUB6.TaoCertificate.combined434_part5 line 124
  53. def OAI.MUB6.TaoCertificate.combined434_part6 line 126
  54. def OAI.MUB6.TaoCertificate.combined434_part7 line 128
  55. def OAI.MUB6.TaoCertificate.combined434_part8 line 130
  56. def OAI.MUB6.TaoCertificate.combined434_part9 line 132
  57. def OAI.MUB6.TaoCertificate.combined434_part10 line 134
  58. def OAI.MUB6.TaoCertificate.combined434_part11 line 136
  59. def OAI.MUB6.TaoCertificate.combined434_part12 line 138
  60. def OAI.MUB6.TaoCertificate.combined434_part13 line 140
  61. def OAI.MUB6.TaoCertificate.combined434_part14 line 142
  62. def OAI.MUB6.TaoCertificate.combined434_part15 line 144
  63. def OAI.MUB6.TaoCertificate.combined434_part16 line 146
  64. def OAI.MUB6.TaoCertificate.combined434_part17 line 148
  65. def OAI.MUB6.TaoCertificate.combined434_part18 line 150
  66. def OAI.MUB6.TaoCertificate.combined434_part19 line 152
  67. def OAI.MUB6.TaoCertificate.combined434 line 154
  68. theorem OAI.MUB6.TaoCertificate.combined434_checked line 156
  69. theorem OAI.MUB6.TaoCertificate.combined434_zero line 159
  70. def OAI.MUB6.TaoCertificate.combined435_part0 line 167
  71. def OAI.MUB6.TaoCertificate.combined435_part1 line 169
  72. def OAI.MUB6.TaoCertificate.combined435_part2 line 171
  73. def OAI.MUB6.TaoCertificate.combined435_part3 line 173
  74. def OAI.MUB6.TaoCertificate.combined435_part4 line 175
  75. def OAI.MUB6.TaoCertificate.combined435_part5 line 177
  76. def OAI.MUB6.TaoCertificate.combined435_part6 line 179
  77. def OAI.MUB6.TaoCertificate.combined435_part7 line 181
  78. def OAI.MUB6.TaoCertificate.combined435_part8 line 183
  79. def OAI.MUB6.TaoCertificate.combined435_part9 line 185
  80. def OAI.MUB6.TaoCertificate.combined435_part10 line 187
  81. def OAI.MUB6.TaoCertificate.combined435_part11 line 189
  82. def OAI.MUB6.TaoCertificate.combined435_part12 line 191
  83. def OAI.MUB6.TaoCertificate.combined435_part13 line 193
  84. def OAI.MUB6.TaoCertificate.combined435_part14 line 195
  85. def OAI.MUB6.TaoCertificate.combined435_part15 line 197
  86. def OAI.MUB6.TaoCertificate.combined435_part16 line 199
  87. def OAI.MUB6.TaoCertificate.combined435_part17 line 201
  88. def OAI.MUB6.TaoCertificate.combined435_part18 line 203
  89. def OAI.MUB6.TaoCertificate.combined435_part19 line 205
  90. def OAI.MUB6.TaoCertificate.combined435 line 207
  91. theorem OAI.MUB6.TaoCertificate.combined435_checked line 209
  92. theorem OAI.MUB6.TaoCertificate.combined435_zero line 212
  93. def OAI.MUB6.TaoCertificate.combined436_part0 line 220
  94. def OAI.MUB6.TaoCertificate.combined436_part1 line 222
  95. def OAI.MUB6.TaoCertificate.combined436_part2 line 224
  96. def OAI.MUB6.TaoCertificate.combined436_part3 line 226
  97. def OAI.MUB6.TaoCertificate.combined436_part4 line 228
  98. def OAI.MUB6.TaoCertificate.combined436_part5 line 230
  99. def OAI.MUB6.TaoCertificate.combined436_part6 line 232
  100. def OAI.MUB6.TaoCertificate.combined436_part7 line 234
  101. def OAI.MUB6.TaoCertificate.combined436_part8 line 236
  102. def OAI.MUB6.TaoCertificate.combined436_part9 line 238
  103. def OAI.MUB6.TaoCertificate.combined436_part10 line 240
  104. def OAI.MUB6.TaoCertificate.combined436_part11 line 242
  105. def OAI.MUB6.TaoCertificate.combined436_part12 line 244
  106. def OAI.MUB6.TaoCertificate.combined436_part13 line 246
  107. def OAI.MUB6.TaoCertificate.combined436_part14 line 248
  108. def OAI.MUB6.TaoCertificate.combined436_part15 line 250
  109. def OAI.MUB6.TaoCertificate.combined436_part16 line 252
  110. def OAI.MUB6.TaoCertificate.combined436_part17 line 254
  111. def OAI.MUB6.TaoCertificate.combined436_part18 line 256
  112. def OAI.MUB6.TaoCertificate.combined436_part19 line 258
  113. def OAI.MUB6.TaoCertificate.combined436 line 260
  114. theorem OAI.MUB6.TaoCertificate.combined436_checked line 262
  115. theorem OAI.MUB6.TaoCertificate.combined436_zero line 265
  116. def OAI.MUB6.TaoCertificate.combined437_part0 line 273
  117. def OAI.MUB6.TaoCertificate.combined437_part1 line 275
  118. def OAI.MUB6.TaoCertificate.combined437_part2 line 277
  119. def OAI.MUB6.TaoCertificate.combined437_part3 line 279
  120. def OAI.MUB6.TaoCertificate.combined437_part4 line 281
  121. def OAI.MUB6.TaoCertificate.combined437_part5 line 283
  122. def OAI.MUB6.TaoCertificate.combined437_part6 line 285
  123. def OAI.MUB6.TaoCertificate.combined437_part7 line 287
  124. def OAI.MUB6.TaoCertificate.combined437_part8 line 289
  125. def OAI.MUB6.TaoCertificate.combined437_part9 line 291
  126. def OAI.MUB6.TaoCertificate.combined437_part10 line 293
  127. def OAI.MUB6.TaoCertificate.combined437_part11 line 295
  128. def OAI.MUB6.TaoCertificate.combined437_part12 line 297
  129. def OAI.MUB6.TaoCertificate.combined437_part13 line 299
  130. def OAI.MUB6.TaoCertificate.combined437_part14 line 301
  131. def OAI.MUB6.TaoCertificate.combined437_part15 line 303
  132. def OAI.MUB6.TaoCertificate.combined437_part16 line 305
  133. def OAI.MUB6.TaoCertificate.combined437_part17 line 307
  134. def OAI.MUB6.TaoCertificate.combined437_part18 line 309
  135. def OAI.MUB6.TaoCertificate.combined437_part19 line 311
  136. def OAI.MUB6.TaoCertificate.combined437 line 313
  137. theorem OAI.MUB6.TaoCertificate.combined437_checked line 315
  138. theorem OAI.MUB6.TaoCertificate.combined437_zero line 318
  139. def OAI.MUB6.TaoCertificate.combined438_part0 line 326
  140. def OAI.MUB6.TaoCertificate.combined438_part1 line 328
  141. def OAI.MUB6.TaoCertificate.combined438_part2 line 330
  142. def OAI.MUB6.TaoCertificate.combined438_part3 line 332
  143. def OAI.MUB6.TaoCertificate.combined438_part4 line 334
  144. def OAI.MUB6.TaoCertificate.combined438_part5 line 336
  145. def OAI.MUB6.TaoCertificate.combined438_part6 line 338
  146. def OAI.MUB6.TaoCertificate.combined438_part7 line 340
  147. def OAI.MUB6.TaoCertificate.combined438_part8 line 342
  148. def OAI.MUB6.TaoCertificate.combined438_part9 line 344
  149. def OAI.MUB6.TaoCertificate.combined438_part10 line 346
  150. def OAI.MUB6.TaoCertificate.combined438_part11 line 348
  151. def OAI.MUB6.TaoCertificate.combined438_part12 line 350
  152. def OAI.MUB6.TaoCertificate.combined438_part13 line 352
  153. def OAI.MUB6.TaoCertificate.combined438_part14 line 354
  154. def OAI.MUB6.TaoCertificate.combined438_part15 line 356
  155. def OAI.MUB6.TaoCertificate.combined438_part16 line 358
  156. def OAI.MUB6.TaoCertificate.combined438_part17 line 360
  157. def OAI.MUB6.TaoCertificate.combined438_part18 line 362
  158. def OAI.MUB6.TaoCertificate.combined438_part19 line 364
  159. def OAI.MUB6.TaoCertificate.combined438 line 366
  160. theorem OAI.MUB6.TaoCertificate.combined438_checked line 368
  161. theorem OAI.MUB6.TaoCertificate.combined438_zero line 371
  162. def OAI.MUB6.TaoCertificate.combined439_part0 line 379
  163. def OAI.MUB6.TaoCertificate.combined439_part1 line 381
  164. def OAI.MUB6.TaoCertificate.combined439_part2 line 383
  165. def OAI.MUB6.TaoCertificate.combined439_part3 line 385
  166. def OAI.MUB6.TaoCertificate.combined439_part4 line 387
  167. def OAI.MUB6.TaoCertificate.combined439_part5 line 389
  168. def OAI.MUB6.TaoCertificate.combined439_part6 line 391
  169. def OAI.MUB6.TaoCertificate.combined439_part7 line 393
  170. def OAI.MUB6.TaoCertificate.combined439_part8 line 395
  171. def OAI.MUB6.TaoCertificate.combined439_part9 line 397
  172. def OAI.MUB6.TaoCertificate.combined439_part10 line 399
  173. def OAI.MUB6.TaoCertificate.combined439_part11 line 401
  174. def OAI.MUB6.TaoCertificate.combined439_part12 line 403
  175. def OAI.MUB6.TaoCertificate.combined439_part13 line 405
  176. def OAI.MUB6.TaoCertificate.combined439_part14 line 407
  177. def OAI.MUB6.TaoCertificate.combined439_part15 line 409
  178. def OAI.MUB6.TaoCertificate.combined439_part16 line 411
  179. def OAI.MUB6.TaoCertificate.combined439_part17 line 413
  180. def OAI.MUB6.TaoCertificate.combined439_part18 line 415
  181. def OAI.MUB6.TaoCertificate.combined439_part19 line 417
  182. def OAI.MUB6.TaoCertificate.combined439 line 419
  183. theorem OAI.MUB6.TaoCertificate.combined439_checked line 421
  184. theorem OAI.MUB6.TaoCertificate.combined439_zero line 424