OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge51.lean

GitHub source file

157 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined408_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined408_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined408_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined408_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined408_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined408_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined408_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined408_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined408_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined408_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined408_part10 line 28
  12. def OAI.MUB6.TaoCertificate.combined408_part11 line 30
  13. def OAI.MUB6.TaoCertificate.combined408_part12 line 32
  14. def OAI.MUB6.TaoCertificate.combined408_part13 line 34
  15. def OAI.MUB6.TaoCertificate.combined408_part14 line 36
  16. def OAI.MUB6.TaoCertificate.combined408_part15 line 38
  17. def OAI.MUB6.TaoCertificate.combined408 line 40
  18. theorem OAI.MUB6.TaoCertificate.combined408_checked line 42
  19. theorem OAI.MUB6.TaoCertificate.combined408_zero line 45
  20. def OAI.MUB6.TaoCertificate.combined409_part0 line 53
  21. def OAI.MUB6.TaoCertificate.combined409_part1 line 55
  22. def OAI.MUB6.TaoCertificate.combined409_part2 line 57
  23. def OAI.MUB6.TaoCertificate.combined409_part3 line 59
  24. def OAI.MUB6.TaoCertificate.combined409_part4 line 61
  25. def OAI.MUB6.TaoCertificate.combined409_part5 line 63
  26. def OAI.MUB6.TaoCertificate.combined409_part6 line 65
  27. def OAI.MUB6.TaoCertificate.combined409_part7 line 67
  28. def OAI.MUB6.TaoCertificate.combined409_part8 line 69
  29. def OAI.MUB6.TaoCertificate.combined409_part9 line 71
  30. def OAI.MUB6.TaoCertificate.combined409_part10 line 73
  31. def OAI.MUB6.TaoCertificate.combined409_part11 line 75
  32. def OAI.MUB6.TaoCertificate.combined409_part12 line 77
  33. def OAI.MUB6.TaoCertificate.combined409_part13 line 79
  34. def OAI.MUB6.TaoCertificate.combined409_part14 line 81
  35. def OAI.MUB6.TaoCertificate.combined409_part15 line 83
  36. def OAI.MUB6.TaoCertificate.combined409 line 85
  37. theorem OAI.MUB6.TaoCertificate.combined409_checked line 87
  38. theorem OAI.MUB6.TaoCertificate.combined409_zero line 90
  39. def OAI.MUB6.TaoCertificate.combined410_part0 line 98
  40. def OAI.MUB6.TaoCertificate.combined410_part1 line 100
  41. def OAI.MUB6.TaoCertificate.combined410_part2 line 102
  42. def OAI.MUB6.TaoCertificate.combined410_part3 line 104
  43. def OAI.MUB6.TaoCertificate.combined410_part4 line 106
  44. def OAI.MUB6.TaoCertificate.combined410_part5 line 108
  45. def OAI.MUB6.TaoCertificate.combined410_part6 line 110
  46. def OAI.MUB6.TaoCertificate.combined410_part7 line 112
  47. def OAI.MUB6.TaoCertificate.combined410_part8 line 114
  48. def OAI.MUB6.TaoCertificate.combined410_part9 line 116
  49. def OAI.MUB6.TaoCertificate.combined410_part10 line 118
  50. def OAI.MUB6.TaoCertificate.combined410_part11 line 120
  51. def OAI.MUB6.TaoCertificate.combined410_part12 line 122
  52. def OAI.MUB6.TaoCertificate.combined410_part13 line 124
  53. def OAI.MUB6.TaoCertificate.combined410_part14 line 126
  54. def OAI.MUB6.TaoCertificate.combined410_part15 line 128
  55. def OAI.MUB6.TaoCertificate.combined410 line 130
  56. theorem OAI.MUB6.TaoCertificate.combined410_checked line 132
  57. theorem OAI.MUB6.TaoCertificate.combined410_zero line 135
  58. def OAI.MUB6.TaoCertificate.combined411_part0 line 143
  59. def OAI.MUB6.TaoCertificate.combined411_part1 line 145
  60. def OAI.MUB6.TaoCertificate.combined411_part2 line 147
  61. def OAI.MUB6.TaoCertificate.combined411_part3 line 149
  62. def OAI.MUB6.TaoCertificate.combined411_part4 line 151
  63. def OAI.MUB6.TaoCertificate.combined411_part5 line 153
  64. def OAI.MUB6.TaoCertificate.combined411_part6 line 155
  65. def OAI.MUB6.TaoCertificate.combined411_part7 line 157
  66. def OAI.MUB6.TaoCertificate.combined411_part8 line 159
  67. def OAI.MUB6.TaoCertificate.combined411_part9 line 161
  68. def OAI.MUB6.TaoCertificate.combined411_part10 line 163
  69. def OAI.MUB6.TaoCertificate.combined411_part11 line 165
  70. def OAI.MUB6.TaoCertificate.combined411_part12 line 167
  71. def OAI.MUB6.TaoCertificate.combined411_part13 line 169
  72. def OAI.MUB6.TaoCertificate.combined411_part14 line 171
  73. def OAI.MUB6.TaoCertificate.combined411_part15 line 173
  74. def OAI.MUB6.TaoCertificate.combined411_part16 line 175
  75. def OAI.MUB6.TaoCertificate.combined411 line 177
  76. theorem OAI.MUB6.TaoCertificate.combined411_checked line 179
  77. theorem OAI.MUB6.TaoCertificate.combined411_zero line 182
  78. def OAI.MUB6.TaoCertificate.combined412_part0 line 190
  79. def OAI.MUB6.TaoCertificate.combined412_part1 line 192
  80. def OAI.MUB6.TaoCertificate.combined412_part2 line 194
  81. def OAI.MUB6.TaoCertificate.combined412_part3 line 196
  82. def OAI.MUB6.TaoCertificate.combined412_part4 line 198
  83. def OAI.MUB6.TaoCertificate.combined412_part5 line 200
  84. def OAI.MUB6.TaoCertificate.combined412_part6 line 202
  85. def OAI.MUB6.TaoCertificate.combined412_part7 line 204
  86. def OAI.MUB6.TaoCertificate.combined412_part8 line 206
  87. def OAI.MUB6.TaoCertificate.combined412_part9 line 208
  88. def OAI.MUB6.TaoCertificate.combined412_part10 line 210
  89. def OAI.MUB6.TaoCertificate.combined412_part11 line 212
  90. def OAI.MUB6.TaoCertificate.combined412_part12 line 214
  91. def OAI.MUB6.TaoCertificate.combined412_part13 line 216
  92. def OAI.MUB6.TaoCertificate.combined412_part14 line 218
  93. def OAI.MUB6.TaoCertificate.combined412_part15 line 220
  94. def OAI.MUB6.TaoCertificate.combined412_part16 line 222
  95. def OAI.MUB6.TaoCertificate.combined412 line 224
  96. theorem OAI.MUB6.TaoCertificate.combined412_checked line 226
  97. theorem OAI.MUB6.TaoCertificate.combined412_zero line 229
  98. def OAI.MUB6.TaoCertificate.combined413_part0 line 237
  99. def OAI.MUB6.TaoCertificate.combined413_part1 line 239
  100. def OAI.MUB6.TaoCertificate.combined413_part2 line 241
  101. def OAI.MUB6.TaoCertificate.combined413_part3 line 243
  102. def OAI.MUB6.TaoCertificate.combined413_part4 line 245
  103. def OAI.MUB6.TaoCertificate.combined413_part5 line 247
  104. def OAI.MUB6.TaoCertificate.combined413_part6 line 249
  105. def OAI.MUB6.TaoCertificate.combined413_part7 line 251
  106. def OAI.MUB6.TaoCertificate.combined413_part8 line 253
  107. def OAI.MUB6.TaoCertificate.combined413_part9 line 255
  108. def OAI.MUB6.TaoCertificate.combined413_part10 line 257
  109. def OAI.MUB6.TaoCertificate.combined413_part11 line 259
  110. def OAI.MUB6.TaoCertificate.combined413_part12 line 261
  111. def OAI.MUB6.TaoCertificate.combined413_part13 line 263
  112. def OAI.MUB6.TaoCertificate.combined413_part14 line 265
  113. def OAI.MUB6.TaoCertificate.combined413_part15 line 267
  114. def OAI.MUB6.TaoCertificate.combined413_part16 line 269
  115. def OAI.MUB6.TaoCertificate.combined413 line 271
  116. theorem OAI.MUB6.TaoCertificate.combined413_checked line 273
  117. theorem OAI.MUB6.TaoCertificate.combined413_zero line 276
  118. def OAI.MUB6.TaoCertificate.combined414_part0 line 284
  119. def OAI.MUB6.TaoCertificate.combined414_part1 line 286
  120. def OAI.MUB6.TaoCertificate.combined414_part2 line 288
  121. def OAI.MUB6.TaoCertificate.combined414_part3 line 290
  122. def OAI.MUB6.TaoCertificate.combined414_part4 line 292
  123. def OAI.MUB6.TaoCertificate.combined414_part5 line 294
  124. def OAI.MUB6.TaoCertificate.combined414_part6 line 296
  125. def OAI.MUB6.TaoCertificate.combined414_part7 line 298
  126. def OAI.MUB6.TaoCertificate.combined414_part8 line 300
  127. def OAI.MUB6.TaoCertificate.combined414_part9 line 302
  128. def OAI.MUB6.TaoCertificate.combined414_part10 line 304
  129. def OAI.MUB6.TaoCertificate.combined414_part11 line 306
  130. def OAI.MUB6.TaoCertificate.combined414_part12 line 308
  131. def OAI.MUB6.TaoCertificate.combined414_part13 line 310
  132. def OAI.MUB6.TaoCertificate.combined414_part14 line 312
  133. def OAI.MUB6.TaoCertificate.combined414_part15 line 314
  134. def OAI.MUB6.TaoCertificate.combined414_part16 line 316
  135. def OAI.MUB6.TaoCertificate.combined414 line 318
  136. theorem OAI.MUB6.TaoCertificate.combined414_checked line 320
  137. theorem OAI.MUB6.TaoCertificate.combined414_zero line 323
  138. def OAI.MUB6.TaoCertificate.combined415_part0 line 331
  139. def OAI.MUB6.TaoCertificate.combined415_part1 line 333
  140. def OAI.MUB6.TaoCertificate.combined415_part2 line 335
  141. def OAI.MUB6.TaoCertificate.combined415_part3 line 337
  142. def OAI.MUB6.TaoCertificate.combined415_part4 line 339
  143. def OAI.MUB6.TaoCertificate.combined415_part5 line 341
  144. def OAI.MUB6.TaoCertificate.combined415_part6 line 343
  145. def OAI.MUB6.TaoCertificate.combined415_part7 line 345
  146. def OAI.MUB6.TaoCertificate.combined415_part8 line 347
  147. def OAI.MUB6.TaoCertificate.combined415_part9 line 349
  148. def OAI.MUB6.TaoCertificate.combined415_part10 line 351
  149. def OAI.MUB6.TaoCertificate.combined415_part11 line 353
  150. def OAI.MUB6.TaoCertificate.combined415_part12 line 355
  151. def OAI.MUB6.TaoCertificate.combined415_part13 line 357
  152. def OAI.MUB6.TaoCertificate.combined415_part14 line 359
  153. def OAI.MUB6.TaoCertificate.combined415_part15 line 361
  154. def OAI.MUB6.TaoCertificate.combined415_part16 line 363
  155. def OAI.MUB6.TaoCertificate.combined415 line 365
  156. theorem OAI.MUB6.TaoCertificate.combined415_checked line 367
  157. theorem OAI.MUB6.TaoCertificate.combined415_zero line 370