OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge58.lean

GitHub source file

164 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined464_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined464_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined464_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined464_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined464_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined464_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined464_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined464_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined464_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined464_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined464_part10 line 28
  12. def OAI.MUB6.TaoCertificate.combined464_part11 line 30
  13. def OAI.MUB6.TaoCertificate.combined464_part12 line 32
  14. def OAI.MUB6.TaoCertificate.combined464_part13 line 34
  15. def OAI.MUB6.TaoCertificate.combined464_part14 line 36
  16. def OAI.MUB6.TaoCertificate.combined464_part15 line 38
  17. def OAI.MUB6.TaoCertificate.combined464_part16 line 40
  18. def OAI.MUB6.TaoCertificate.combined464_part17 line 42
  19. def OAI.MUB6.TaoCertificate.combined464 line 44
  20. theorem OAI.MUB6.TaoCertificate.combined464_checked line 46
  21. theorem OAI.MUB6.TaoCertificate.combined464_zero line 49
  22. def OAI.MUB6.TaoCertificate.combined465_part0 line 57
  23. def OAI.MUB6.TaoCertificate.combined465_part1 line 59
  24. def OAI.MUB6.TaoCertificate.combined465_part2 line 61
  25. def OAI.MUB6.TaoCertificate.combined465_part3 line 63
  26. def OAI.MUB6.TaoCertificate.combined465_part4 line 65
  27. def OAI.MUB6.TaoCertificate.combined465_part5 line 67
  28. def OAI.MUB6.TaoCertificate.combined465_part6 line 69
  29. def OAI.MUB6.TaoCertificate.combined465_part7 line 71
  30. def OAI.MUB6.TaoCertificate.combined465_part8 line 73
  31. def OAI.MUB6.TaoCertificate.combined465_part9 line 75
  32. def OAI.MUB6.TaoCertificate.combined465_part10 line 77
  33. def OAI.MUB6.TaoCertificate.combined465_part11 line 79
  34. def OAI.MUB6.TaoCertificate.combined465_part12 line 81
  35. def OAI.MUB6.TaoCertificate.combined465_part13 line 83
  36. def OAI.MUB6.TaoCertificate.combined465_part14 line 85
  37. def OAI.MUB6.TaoCertificate.combined465_part15 line 87
  38. def OAI.MUB6.TaoCertificate.combined465_part16 line 89
  39. def OAI.MUB6.TaoCertificate.combined465_part17 line 91
  40. def OAI.MUB6.TaoCertificate.combined465 line 93
  41. theorem OAI.MUB6.TaoCertificate.combined465_checked line 95
  42. theorem OAI.MUB6.TaoCertificate.combined465_zero line 98
  43. def OAI.MUB6.TaoCertificate.combined466_part0 line 106
  44. def OAI.MUB6.TaoCertificate.combined466_part1 line 108
  45. def OAI.MUB6.TaoCertificate.combined466_part2 line 110
  46. def OAI.MUB6.TaoCertificate.combined466_part3 line 112
  47. def OAI.MUB6.TaoCertificate.combined466_part4 line 114
  48. def OAI.MUB6.TaoCertificate.combined466_part5 line 116
  49. def OAI.MUB6.TaoCertificate.combined466_part6 line 118
  50. def OAI.MUB6.TaoCertificate.combined466_part7 line 120
  51. def OAI.MUB6.TaoCertificate.combined466_part8 line 122
  52. def OAI.MUB6.TaoCertificate.combined466_part9 line 124
  53. def OAI.MUB6.TaoCertificate.combined466_part10 line 126
  54. def OAI.MUB6.TaoCertificate.combined466_part11 line 128
  55. def OAI.MUB6.TaoCertificate.combined466_part12 line 130
  56. def OAI.MUB6.TaoCertificate.combined466_part13 line 132
  57. def OAI.MUB6.TaoCertificate.combined466_part14 line 134
  58. def OAI.MUB6.TaoCertificate.combined466_part15 line 136
  59. def OAI.MUB6.TaoCertificate.combined466_part16 line 138
  60. def OAI.MUB6.TaoCertificate.combined466_part17 line 140
  61. def OAI.MUB6.TaoCertificate.combined466 line 142
  62. theorem OAI.MUB6.TaoCertificate.combined466_checked line 144
  63. theorem OAI.MUB6.TaoCertificate.combined466_zero line 147
  64. def OAI.MUB6.TaoCertificate.combined467_part0 line 155
  65. def OAI.MUB6.TaoCertificate.combined467_part1 line 157
  66. def OAI.MUB6.TaoCertificate.combined467_part2 line 159
  67. def OAI.MUB6.TaoCertificate.combined467_part3 line 161
  68. def OAI.MUB6.TaoCertificate.combined467_part4 line 163
  69. def OAI.MUB6.TaoCertificate.combined467_part5 line 165
  70. def OAI.MUB6.TaoCertificate.combined467_part6 line 167
  71. def OAI.MUB6.TaoCertificate.combined467_part7 line 169
  72. def OAI.MUB6.TaoCertificate.combined467_part8 line 171
  73. def OAI.MUB6.TaoCertificate.combined467_part9 line 173
  74. def OAI.MUB6.TaoCertificate.combined467_part10 line 175
  75. def OAI.MUB6.TaoCertificate.combined467_part11 line 177
  76. def OAI.MUB6.TaoCertificate.combined467_part12 line 179
  77. def OAI.MUB6.TaoCertificate.combined467_part13 line 181
  78. def OAI.MUB6.TaoCertificate.combined467_part14 line 183
  79. def OAI.MUB6.TaoCertificate.combined467_part15 line 185
  80. def OAI.MUB6.TaoCertificate.combined467_part16 line 187
  81. def OAI.MUB6.TaoCertificate.combined467_part17 line 189
  82. def OAI.MUB6.TaoCertificate.combined467 line 191
  83. theorem OAI.MUB6.TaoCertificate.combined467_checked line 193
  84. theorem OAI.MUB6.TaoCertificate.combined467_zero line 196
  85. def OAI.MUB6.TaoCertificate.combined468_part0 line 204
  86. def OAI.MUB6.TaoCertificate.combined468_part1 line 206
  87. def OAI.MUB6.TaoCertificate.combined468_part2 line 208
  88. def OAI.MUB6.TaoCertificate.combined468_part3 line 210
  89. def OAI.MUB6.TaoCertificate.combined468_part4 line 212
  90. def OAI.MUB6.TaoCertificate.combined468_part5 line 214
  91. def OAI.MUB6.TaoCertificate.combined468_part6 line 216
  92. def OAI.MUB6.TaoCertificate.combined468_part7 line 218
  93. def OAI.MUB6.TaoCertificate.combined468_part8 line 220
  94. def OAI.MUB6.TaoCertificate.combined468_part9 line 222
  95. def OAI.MUB6.TaoCertificate.combined468_part10 line 224
  96. def OAI.MUB6.TaoCertificate.combined468_part11 line 226
  97. def OAI.MUB6.TaoCertificate.combined468_part12 line 228
  98. def OAI.MUB6.TaoCertificate.combined468_part13 line 230
  99. def OAI.MUB6.TaoCertificate.combined468_part14 line 232
  100. def OAI.MUB6.TaoCertificate.combined468_part15 line 234
  101. def OAI.MUB6.TaoCertificate.combined468_part16 line 236
  102. def OAI.MUB6.TaoCertificate.combined468_part17 line 238
  103. def OAI.MUB6.TaoCertificate.combined468 line 240
  104. theorem OAI.MUB6.TaoCertificate.combined468_checked line 242
  105. theorem OAI.MUB6.TaoCertificate.combined468_zero line 245
  106. def OAI.MUB6.TaoCertificate.combined469_part0 line 253
  107. def OAI.MUB6.TaoCertificate.combined469_part1 line 255
  108. def OAI.MUB6.TaoCertificate.combined469_part2 line 257
  109. def OAI.MUB6.TaoCertificate.combined469_part3 line 259
  110. def OAI.MUB6.TaoCertificate.combined469_part4 line 261
  111. def OAI.MUB6.TaoCertificate.combined469_part5 line 263
  112. def OAI.MUB6.TaoCertificate.combined469_part6 line 265
  113. def OAI.MUB6.TaoCertificate.combined469_part7 line 267
  114. def OAI.MUB6.TaoCertificate.combined469_part8 line 269
  115. def OAI.MUB6.TaoCertificate.combined469_part9 line 271
  116. def OAI.MUB6.TaoCertificate.combined469_part10 line 273
  117. def OAI.MUB6.TaoCertificate.combined469_part11 line 275
  118. def OAI.MUB6.TaoCertificate.combined469_part12 line 277
  119. def OAI.MUB6.TaoCertificate.combined469_part13 line 279
  120. def OAI.MUB6.TaoCertificate.combined469_part14 line 281
  121. def OAI.MUB6.TaoCertificate.combined469_part15 line 283
  122. def OAI.MUB6.TaoCertificate.combined469_part16 line 285
  123. def OAI.MUB6.TaoCertificate.combined469 line 287
  124. theorem OAI.MUB6.TaoCertificate.combined469_checked line 289
  125. theorem OAI.MUB6.TaoCertificate.combined469_zero line 292
  126. def OAI.MUB6.TaoCertificate.combined470_part0 line 300
  127. def OAI.MUB6.TaoCertificate.combined470_part1 line 302
  128. def OAI.MUB6.TaoCertificate.combined470_part2 line 304
  129. def OAI.MUB6.TaoCertificate.combined470_part3 line 306
  130. def OAI.MUB6.TaoCertificate.combined470_part4 line 308
  131. def OAI.MUB6.TaoCertificate.combined470_part5 line 310
  132. def OAI.MUB6.TaoCertificate.combined470_part6 line 312
  133. def OAI.MUB6.TaoCertificate.combined470_part7 line 314
  134. def OAI.MUB6.TaoCertificate.combined470_part8 line 316
  135. def OAI.MUB6.TaoCertificate.combined470_part9 line 318
  136. def OAI.MUB6.TaoCertificate.combined470_part10 line 320
  137. def OAI.MUB6.TaoCertificate.combined470_part11 line 322
  138. def OAI.MUB6.TaoCertificate.combined470_part12 line 324
  139. def OAI.MUB6.TaoCertificate.combined470_part13 line 326
  140. def OAI.MUB6.TaoCertificate.combined470_part14 line 328
  141. def OAI.MUB6.TaoCertificate.combined470_part15 line 330
  142. def OAI.MUB6.TaoCertificate.combined470_part16 line 332
  143. def OAI.MUB6.TaoCertificate.combined470 line 334
  144. theorem OAI.MUB6.TaoCertificate.combined470_checked line 336
  145. theorem OAI.MUB6.TaoCertificate.combined470_zero line 339
  146. def OAI.MUB6.TaoCertificate.combined471_part0 line 347
  147. def OAI.MUB6.TaoCertificate.combined471_part1 line 349
  148. def OAI.MUB6.TaoCertificate.combined471_part2 line 351
  149. def OAI.MUB6.TaoCertificate.combined471_part3 line 353
  150. def OAI.MUB6.TaoCertificate.combined471_part4 line 355
  151. def OAI.MUB6.TaoCertificate.combined471_part5 line 357
  152. def OAI.MUB6.TaoCertificate.combined471_part6 line 359
  153. def OAI.MUB6.TaoCertificate.combined471_part7 line 361
  154. def OAI.MUB6.TaoCertificate.combined471_part8 line 363
  155. def OAI.MUB6.TaoCertificate.combined471_part9 line 365
  156. def OAI.MUB6.TaoCertificate.combined471_part10 line 367
  157. def OAI.MUB6.TaoCertificate.combined471_part11 line 369
  158. def OAI.MUB6.TaoCertificate.combined471_part12 line 371
  159. def OAI.MUB6.TaoCertificate.combined471_part13 line 373
  160. def OAI.MUB6.TaoCertificate.combined471_part14 line 375
  161. def OAI.MUB6.TaoCertificate.combined471_part15 line 377
  162. def OAI.MUB6.TaoCertificate.combined471 line 379
  163. theorem OAI.MUB6.TaoCertificate.combined471_checked line 381
  164. theorem OAI.MUB6.TaoCertificate.combined471_zero line 384