OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge49.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined392_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined392_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined392_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined392_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined392_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined392_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined392_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined392_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined392_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined392_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined392_part10 line 28
  12. def OAI.MUB6.TaoCertificate.combined392_part11 line 30
  13. def OAI.MUB6.TaoCertificate.combined392_part12 line 32
  14. def OAI.MUB6.TaoCertificate.combined392_part13 line 34
  15. def OAI.MUB6.TaoCertificate.combined392_part14 line 36
  16. def OAI.MUB6.TaoCertificate.combined392 line 38
  17. theorem OAI.MUB6.TaoCertificate.combined392_checked line 40
  18. theorem OAI.MUB6.TaoCertificate.combined392_zero line 43
  19. def OAI.MUB6.TaoCertificate.combined393_part0 line 51
  20. def OAI.MUB6.TaoCertificate.combined393_part1 line 53
  21. def OAI.MUB6.TaoCertificate.combined393_part2 line 55
  22. def OAI.MUB6.TaoCertificate.combined393_part3 line 57
  23. def OAI.MUB6.TaoCertificate.combined393_part4 line 59
  24. def OAI.MUB6.TaoCertificate.combined393_part5 line 61
  25. def OAI.MUB6.TaoCertificate.combined393_part6 line 63
  26. def OAI.MUB6.TaoCertificate.combined393_part7 line 65
  27. def OAI.MUB6.TaoCertificate.combined393_part8 line 67
  28. def OAI.MUB6.TaoCertificate.combined393_part9 line 69
  29. def OAI.MUB6.TaoCertificate.combined393_part10 line 71
  30. def OAI.MUB6.TaoCertificate.combined393_part11 line 73
  31. def OAI.MUB6.TaoCertificate.combined393_part12 line 75
  32. def OAI.MUB6.TaoCertificate.combined393_part13 line 77
  33. def OAI.MUB6.TaoCertificate.combined393_part14 line 79
  34. def OAI.MUB6.TaoCertificate.combined393 line 81
  35. theorem OAI.MUB6.TaoCertificate.combined393_checked line 83
  36. theorem OAI.MUB6.TaoCertificate.combined393_zero line 86
  37. def OAI.MUB6.TaoCertificate.combined394_part0 line 94
  38. def OAI.MUB6.TaoCertificate.combined394_part1 line 96
  39. def OAI.MUB6.TaoCertificate.combined394_part2 line 98
  40. def OAI.MUB6.TaoCertificate.combined394_part3 line 100
  41. def OAI.MUB6.TaoCertificate.combined394_part4 line 102
  42. def OAI.MUB6.TaoCertificate.combined394_part5 line 104
  43. def OAI.MUB6.TaoCertificate.combined394_part6 line 106
  44. def OAI.MUB6.TaoCertificate.combined394_part7 line 108
  45. def OAI.MUB6.TaoCertificate.combined394_part8 line 110
  46. def OAI.MUB6.TaoCertificate.combined394_part9 line 112
  47. def OAI.MUB6.TaoCertificate.combined394_part10 line 114
  48. def OAI.MUB6.TaoCertificate.combined394_part11 line 116
  49. def OAI.MUB6.TaoCertificate.combined394_part12 line 118
  50. def OAI.MUB6.TaoCertificate.combined394_part13 line 120
  51. def OAI.MUB6.TaoCertificate.combined394_part14 line 122
  52. def OAI.MUB6.TaoCertificate.combined394 line 124
  53. theorem OAI.MUB6.TaoCertificate.combined394_checked line 126
  54. theorem OAI.MUB6.TaoCertificate.combined394_zero line 129
  55. def OAI.MUB6.TaoCertificate.combined395_part0 line 137
  56. def OAI.MUB6.TaoCertificate.combined395_part1 line 139
  57. def OAI.MUB6.TaoCertificate.combined395_part2 line 141
  58. def OAI.MUB6.TaoCertificate.combined395_part3 line 143
  59. def OAI.MUB6.TaoCertificate.combined395_part4 line 145
  60. def OAI.MUB6.TaoCertificate.combined395_part5 line 147
  61. def OAI.MUB6.TaoCertificate.combined395_part6 line 149
  62. def OAI.MUB6.TaoCertificate.combined395_part7 line 151
  63. def OAI.MUB6.TaoCertificate.combined395_part8 line 153
  64. def OAI.MUB6.TaoCertificate.combined395_part9 line 155
  65. def OAI.MUB6.TaoCertificate.combined395_part10 line 157
  66. def OAI.MUB6.TaoCertificate.combined395_part11 line 159
  67. def OAI.MUB6.TaoCertificate.combined395_part12 line 161
  68. def OAI.MUB6.TaoCertificate.combined395_part13 line 163
  69. def OAI.MUB6.TaoCertificate.combined395_part14 line 165
  70. def OAI.MUB6.TaoCertificate.combined395_part15 line 167
  71. def OAI.MUB6.TaoCertificate.combined395 line 169
  72. theorem OAI.MUB6.TaoCertificate.combined395_checked line 171
  73. theorem OAI.MUB6.TaoCertificate.combined395_zero line 174
  74. def OAI.MUB6.TaoCertificate.combined396_part0 line 182
  75. def OAI.MUB6.TaoCertificate.combined396_part1 line 184
  76. def OAI.MUB6.TaoCertificate.combined396_part2 line 186
  77. def OAI.MUB6.TaoCertificate.combined396_part3 line 188
  78. def OAI.MUB6.TaoCertificate.combined396_part4 line 190
  79. def OAI.MUB6.TaoCertificate.combined396_part5 line 192
  80. def OAI.MUB6.TaoCertificate.combined396_part6 line 194
  81. def OAI.MUB6.TaoCertificate.combined396_part7 line 196
  82. def OAI.MUB6.TaoCertificate.combined396_part8 line 198
  83. def OAI.MUB6.TaoCertificate.combined396_part9 line 200
  84. def OAI.MUB6.TaoCertificate.combined396_part10 line 202
  85. def OAI.MUB6.TaoCertificate.combined396_part11 line 204
  86. def OAI.MUB6.TaoCertificate.combined396_part12 line 206
  87. def OAI.MUB6.TaoCertificate.combined396_part13 line 208
  88. def OAI.MUB6.TaoCertificate.combined396_part14 line 210
  89. def OAI.MUB6.TaoCertificate.combined396_part15 line 212
  90. def OAI.MUB6.TaoCertificate.combined396 line 214
  91. theorem OAI.MUB6.TaoCertificate.combined396_checked line 216
  92. theorem OAI.MUB6.TaoCertificate.combined396_zero line 219
  93. def OAI.MUB6.TaoCertificate.combined397_part0 line 227
  94. def OAI.MUB6.TaoCertificate.combined397_part1 line 229
  95. def OAI.MUB6.TaoCertificate.combined397_part2 line 231
  96. def OAI.MUB6.TaoCertificate.combined397_part3 line 233
  97. def OAI.MUB6.TaoCertificate.combined397_part4 line 235
  98. def OAI.MUB6.TaoCertificate.combined397_part5 line 237
  99. def OAI.MUB6.TaoCertificate.combined397_part6 line 239
  100. def OAI.MUB6.TaoCertificate.combined397_part7 line 241
  101. def OAI.MUB6.TaoCertificate.combined397_part8 line 243
  102. def OAI.MUB6.TaoCertificate.combined397_part9 line 245
  103. def OAI.MUB6.TaoCertificate.combined397_part10 line 247
  104. def OAI.MUB6.TaoCertificate.combined397_part11 line 249
  105. def OAI.MUB6.TaoCertificate.combined397_part12 line 251
  106. def OAI.MUB6.TaoCertificate.combined397_part13 line 253
  107. def OAI.MUB6.TaoCertificate.combined397_part14 line 255
  108. def OAI.MUB6.TaoCertificate.combined397 line 257
  109. theorem OAI.MUB6.TaoCertificate.combined397_checked line 259
  110. theorem OAI.MUB6.TaoCertificate.combined397_zero line 262
  111. def OAI.MUB6.TaoCertificate.combined398_part0 line 270
  112. def OAI.MUB6.TaoCertificate.combined398_part1 line 272
  113. def OAI.MUB6.TaoCertificate.combined398_part2 line 274
  114. def OAI.MUB6.TaoCertificate.combined398_part3 line 276
  115. def OAI.MUB6.TaoCertificate.combined398_part4 line 278
  116. def OAI.MUB6.TaoCertificate.combined398_part5 line 280
  117. def OAI.MUB6.TaoCertificate.combined398_part6 line 282
  118. def OAI.MUB6.TaoCertificate.combined398_part7 line 284
  119. def OAI.MUB6.TaoCertificate.combined398_part8 line 286
  120. def OAI.MUB6.TaoCertificate.combined398_part9 line 288
  121. def OAI.MUB6.TaoCertificate.combined398_part10 line 290
  122. def OAI.MUB6.TaoCertificate.combined398_part11 line 292
  123. def OAI.MUB6.TaoCertificate.combined398_part12 line 294
  124. def OAI.MUB6.TaoCertificate.combined398_part13 line 296
  125. def OAI.MUB6.TaoCertificate.combined398_part14 line 298
  126. def OAI.MUB6.TaoCertificate.combined398 line 300
  127. theorem OAI.MUB6.TaoCertificate.combined398_checked line 302
  128. theorem OAI.MUB6.TaoCertificate.combined398_zero line 305
  129. def OAI.MUB6.TaoCertificate.combined399_part0 line 313
  130. def OAI.MUB6.TaoCertificate.combined399_part1 line 315
  131. def OAI.MUB6.TaoCertificate.combined399_part2 line 317
  132. def OAI.MUB6.TaoCertificate.combined399_part3 line 319
  133. def OAI.MUB6.TaoCertificate.combined399_part4 line 321
  134. def OAI.MUB6.TaoCertificate.combined399_part5 line 323
  135. def OAI.MUB6.TaoCertificate.combined399_part6 line 325
  136. def OAI.MUB6.TaoCertificate.combined399_part7 line 327
  137. def OAI.MUB6.TaoCertificate.combined399_part8 line 329
  138. def OAI.MUB6.TaoCertificate.combined399_part9 line 331
  139. def OAI.MUB6.TaoCertificate.combined399_part10 line 333
  140. def OAI.MUB6.TaoCertificate.combined399_part11 line 335
  141. def OAI.MUB6.TaoCertificate.combined399_part12 line 337
  142. def OAI.MUB6.TaoCertificate.combined399_part13 line 339
  143. def OAI.MUB6.TaoCertificate.combined399_part14 line 341
  144. def OAI.MUB6.TaoCertificate.combined399 line 343
  145. theorem OAI.MUB6.TaoCertificate.combined399_checked line 345
  146. theorem OAI.MUB6.TaoCertificate.combined399_zero line 348