OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge57.lean

GitHub source file

172 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined456_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined456_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined456_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined456_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined456_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined456_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined456_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined456_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined456_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined456_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined456_part10 line 28
  12. def OAI.MUB6.TaoCertificate.combined456_part11 line 30
  13. def OAI.MUB6.TaoCertificate.combined456_part12 line 32
  14. def OAI.MUB6.TaoCertificate.combined456_part13 line 34
  15. def OAI.MUB6.TaoCertificate.combined456_part14 line 36
  16. def OAI.MUB6.TaoCertificate.combined456_part15 line 38
  17. def OAI.MUB6.TaoCertificate.combined456_part16 line 40
  18. def OAI.MUB6.TaoCertificate.combined456_part17 line 42
  19. def OAI.MUB6.TaoCertificate.combined456_part18 line 44
  20. def OAI.MUB6.TaoCertificate.combined456 line 46
  21. theorem OAI.MUB6.TaoCertificate.combined456_checked line 48
  22. theorem OAI.MUB6.TaoCertificate.combined456_zero line 51
  23. def OAI.MUB6.TaoCertificate.combined457_part0 line 59
  24. def OAI.MUB6.TaoCertificate.combined457_part1 line 61
  25. def OAI.MUB6.TaoCertificate.combined457_part2 line 63
  26. def OAI.MUB6.TaoCertificate.combined457_part3 line 65
  27. def OAI.MUB6.TaoCertificate.combined457_part4 line 67
  28. def OAI.MUB6.TaoCertificate.combined457_part5 line 69
  29. def OAI.MUB6.TaoCertificate.combined457_part6 line 71
  30. def OAI.MUB6.TaoCertificate.combined457_part7 line 73
  31. def OAI.MUB6.TaoCertificate.combined457_part8 line 75
  32. def OAI.MUB6.TaoCertificate.combined457_part9 line 77
  33. def OAI.MUB6.TaoCertificate.combined457_part10 line 79
  34. def OAI.MUB6.TaoCertificate.combined457_part11 line 81
  35. def OAI.MUB6.TaoCertificate.combined457_part12 line 83
  36. def OAI.MUB6.TaoCertificate.combined457_part13 line 85
  37. def OAI.MUB6.TaoCertificate.combined457_part14 line 87
  38. def OAI.MUB6.TaoCertificate.combined457_part15 line 89
  39. def OAI.MUB6.TaoCertificate.combined457_part16 line 91
  40. def OAI.MUB6.TaoCertificate.combined457_part17 line 93
  41. def OAI.MUB6.TaoCertificate.combined457_part18 line 95
  42. def OAI.MUB6.TaoCertificate.combined457 line 97
  43. theorem OAI.MUB6.TaoCertificate.combined457_checked line 99
  44. theorem OAI.MUB6.TaoCertificate.combined457_zero line 102
  45. def OAI.MUB6.TaoCertificate.combined458_part0 line 110
  46. def OAI.MUB6.TaoCertificate.combined458_part1 line 112
  47. def OAI.MUB6.TaoCertificate.combined458_part2 line 114
  48. def OAI.MUB6.TaoCertificate.combined458_part3 line 116
  49. def OAI.MUB6.TaoCertificate.combined458_part4 line 118
  50. def OAI.MUB6.TaoCertificate.combined458_part5 line 120
  51. def OAI.MUB6.TaoCertificate.combined458_part6 line 122
  52. def OAI.MUB6.TaoCertificate.combined458_part7 line 124
  53. def OAI.MUB6.TaoCertificate.combined458_part8 line 126
  54. def OAI.MUB6.TaoCertificate.combined458_part9 line 128
  55. def OAI.MUB6.TaoCertificate.combined458_part10 line 130
  56. def OAI.MUB6.TaoCertificate.combined458_part11 line 132
  57. def OAI.MUB6.TaoCertificate.combined458_part12 line 134
  58. def OAI.MUB6.TaoCertificate.combined458_part13 line 136
  59. def OAI.MUB6.TaoCertificate.combined458_part14 line 138
  60. def OAI.MUB6.TaoCertificate.combined458_part15 line 140
  61. def OAI.MUB6.TaoCertificate.combined458_part16 line 142
  62. def OAI.MUB6.TaoCertificate.combined458_part17 line 144
  63. def OAI.MUB6.TaoCertificate.combined458_part18 line 146
  64. def OAI.MUB6.TaoCertificate.combined458 line 148
  65. theorem OAI.MUB6.TaoCertificate.combined458_checked line 150
  66. theorem OAI.MUB6.TaoCertificate.combined458_zero line 153
  67. def OAI.MUB6.TaoCertificate.combined459_part0 line 161
  68. def OAI.MUB6.TaoCertificate.combined459_part1 line 163
  69. def OAI.MUB6.TaoCertificate.combined459_part2 line 165
  70. def OAI.MUB6.TaoCertificate.combined459_part3 line 167
  71. def OAI.MUB6.TaoCertificate.combined459_part4 line 169
  72. def OAI.MUB6.TaoCertificate.combined459_part5 line 171
  73. def OAI.MUB6.TaoCertificate.combined459_part6 line 173
  74. def OAI.MUB6.TaoCertificate.combined459_part7 line 175
  75. def OAI.MUB6.TaoCertificate.combined459_part8 line 177
  76. def OAI.MUB6.TaoCertificate.combined459_part9 line 179
  77. def OAI.MUB6.TaoCertificate.combined459_part10 line 181
  78. def OAI.MUB6.TaoCertificate.combined459_part11 line 183
  79. def OAI.MUB6.TaoCertificate.combined459_part12 line 185
  80. def OAI.MUB6.TaoCertificate.combined459_part13 line 187
  81. def OAI.MUB6.TaoCertificate.combined459_part14 line 189
  82. def OAI.MUB6.TaoCertificate.combined459_part15 line 191
  83. def OAI.MUB6.TaoCertificate.combined459_part16 line 193
  84. def OAI.MUB6.TaoCertificate.combined459_part17 line 195
  85. def OAI.MUB6.TaoCertificate.combined459_part18 line 197
  86. def OAI.MUB6.TaoCertificate.combined459 line 199
  87. theorem OAI.MUB6.TaoCertificate.combined459_checked line 201
  88. theorem OAI.MUB6.TaoCertificate.combined459_zero line 204
  89. def OAI.MUB6.TaoCertificate.combined460_part0 line 212
  90. def OAI.MUB6.TaoCertificate.combined460_part1 line 214
  91. def OAI.MUB6.TaoCertificate.combined460_part2 line 216
  92. def OAI.MUB6.TaoCertificate.combined460_part3 line 218
  93. def OAI.MUB6.TaoCertificate.combined460_part4 line 220
  94. def OAI.MUB6.TaoCertificate.combined460_part5 line 222
  95. def OAI.MUB6.TaoCertificate.combined460_part6 line 224
  96. def OAI.MUB6.TaoCertificate.combined460_part7 line 226
  97. def OAI.MUB6.TaoCertificate.combined460_part8 line 228
  98. def OAI.MUB6.TaoCertificate.combined460_part9 line 230
  99. def OAI.MUB6.TaoCertificate.combined460_part10 line 232
  100. def OAI.MUB6.TaoCertificate.combined460_part11 line 234
  101. def OAI.MUB6.TaoCertificate.combined460_part12 line 236
  102. def OAI.MUB6.TaoCertificate.combined460_part13 line 238
  103. def OAI.MUB6.TaoCertificate.combined460_part14 line 240
  104. def OAI.MUB6.TaoCertificate.combined460_part15 line 242
  105. def OAI.MUB6.TaoCertificate.combined460_part16 line 244
  106. def OAI.MUB6.TaoCertificate.combined460_part17 line 246
  107. def OAI.MUB6.TaoCertificate.combined460 line 248
  108. theorem OAI.MUB6.TaoCertificate.combined460_checked line 250
  109. theorem OAI.MUB6.TaoCertificate.combined460_zero line 253
  110. def OAI.MUB6.TaoCertificate.combined461_part0 line 261
  111. def OAI.MUB6.TaoCertificate.combined461_part1 line 263
  112. def OAI.MUB6.TaoCertificate.combined461_part2 line 265
  113. def OAI.MUB6.TaoCertificate.combined461_part3 line 267
  114. def OAI.MUB6.TaoCertificate.combined461_part4 line 269
  115. def OAI.MUB6.TaoCertificate.combined461_part5 line 271
  116. def OAI.MUB6.TaoCertificate.combined461_part6 line 273
  117. def OAI.MUB6.TaoCertificate.combined461_part7 line 275
  118. def OAI.MUB6.TaoCertificate.combined461_part8 line 277
  119. def OAI.MUB6.TaoCertificate.combined461_part9 line 279
  120. def OAI.MUB6.TaoCertificate.combined461_part10 line 281
  121. def OAI.MUB6.TaoCertificate.combined461_part11 line 283
  122. def OAI.MUB6.TaoCertificate.combined461_part12 line 285
  123. def OAI.MUB6.TaoCertificate.combined461_part13 line 287
  124. def OAI.MUB6.TaoCertificate.combined461_part14 line 289
  125. def OAI.MUB6.TaoCertificate.combined461_part15 line 291
  126. def OAI.MUB6.TaoCertificate.combined461_part16 line 293
  127. def OAI.MUB6.TaoCertificate.combined461_part17 line 295
  128. def OAI.MUB6.TaoCertificate.combined461 line 297
  129. theorem OAI.MUB6.TaoCertificate.combined461_checked line 299
  130. theorem OAI.MUB6.TaoCertificate.combined461_zero line 302
  131. def OAI.MUB6.TaoCertificate.combined462_part0 line 310
  132. def OAI.MUB6.TaoCertificate.combined462_part1 line 312
  133. def OAI.MUB6.TaoCertificate.combined462_part2 line 314
  134. def OAI.MUB6.TaoCertificate.combined462_part3 line 316
  135. def OAI.MUB6.TaoCertificate.combined462_part4 line 318
  136. def OAI.MUB6.TaoCertificate.combined462_part5 line 320
  137. def OAI.MUB6.TaoCertificate.combined462_part6 line 322
  138. def OAI.MUB6.TaoCertificate.combined462_part7 line 324
  139. def OAI.MUB6.TaoCertificate.combined462_part8 line 326
  140. def OAI.MUB6.TaoCertificate.combined462_part9 line 328
  141. def OAI.MUB6.TaoCertificate.combined462_part10 line 330
  142. def OAI.MUB6.TaoCertificate.combined462_part11 line 332
  143. def OAI.MUB6.TaoCertificate.combined462_part12 line 334
  144. def OAI.MUB6.TaoCertificate.combined462_part13 line 336
  145. def OAI.MUB6.TaoCertificate.combined462_part14 line 338
  146. def OAI.MUB6.TaoCertificate.combined462_part15 line 340
  147. def OAI.MUB6.TaoCertificate.combined462_part16 line 342
  148. def OAI.MUB6.TaoCertificate.combined462_part17 line 344
  149. def OAI.MUB6.TaoCertificate.combined462 line 346
  150. theorem OAI.MUB6.TaoCertificate.combined462_checked line 348
  151. theorem OAI.MUB6.TaoCertificate.combined462_zero line 351
  152. def OAI.MUB6.TaoCertificate.combined463_part0 line 359
  153. def OAI.MUB6.TaoCertificate.combined463_part1 line 361
  154. def OAI.MUB6.TaoCertificate.combined463_part2 line 363
  155. def OAI.MUB6.TaoCertificate.combined463_part3 line 365
  156. def OAI.MUB6.TaoCertificate.combined463_part4 line 367
  157. def OAI.MUB6.TaoCertificate.combined463_part5 line 369
  158. def OAI.MUB6.TaoCertificate.combined463_part6 line 371
  159. def OAI.MUB6.TaoCertificate.combined463_part7 line 373
  160. def OAI.MUB6.TaoCertificate.combined463_part8 line 375
  161. def OAI.MUB6.TaoCertificate.combined463_part9 line 377
  162. def OAI.MUB6.TaoCertificate.combined463_part10 line 379
  163. def OAI.MUB6.TaoCertificate.combined463_part11 line 381
  164. def OAI.MUB6.TaoCertificate.combined463_part12 line 383
  165. def OAI.MUB6.TaoCertificate.combined463_part13 line 385
  166. def OAI.MUB6.TaoCertificate.combined463_part14 line 387
  167. def OAI.MUB6.TaoCertificate.combined463_part15 line 389
  168. def OAI.MUB6.TaoCertificate.combined463_part16 line 391
  169. def OAI.MUB6.TaoCertificate.combined463_part17 line 393
  170. def OAI.MUB6.TaoCertificate.combined463 line 395
  171. theorem OAI.MUB6.TaoCertificate.combined463_checked line 397
  172. theorem OAI.MUB6.TaoCertificate.combined463_zero line 400