OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge48.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined384_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined384_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined384_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined384_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined384_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined384_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined384_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined384_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined384_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined384_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined384_part10 line 28
  12. def OAI.MUB6.TaoCertificate.combined384_part11 line 30
  13. def OAI.MUB6.TaoCertificate.combined384 line 32
  14. theorem OAI.MUB6.TaoCertificate.combined384_checked line 34
  15. theorem OAI.MUB6.TaoCertificate.combined384_zero line 37
  16. def OAI.MUB6.TaoCertificate.combined385_part0 line 45
  17. def OAI.MUB6.TaoCertificate.combined385_part1 line 47
  18. def OAI.MUB6.TaoCertificate.combined385_part2 line 49
  19. def OAI.MUB6.TaoCertificate.combined385_part3 line 51
  20. def OAI.MUB6.TaoCertificate.combined385_part4 line 53
  21. def OAI.MUB6.TaoCertificate.combined385_part5 line 55
  22. def OAI.MUB6.TaoCertificate.combined385_part6 line 57
  23. def OAI.MUB6.TaoCertificate.combined385_part7 line 59
  24. def OAI.MUB6.TaoCertificate.combined385_part8 line 61
  25. def OAI.MUB6.TaoCertificate.combined385_part9 line 63
  26. def OAI.MUB6.TaoCertificate.combined385_part10 line 65
  27. def OAI.MUB6.TaoCertificate.combined385_part11 line 67
  28. def OAI.MUB6.TaoCertificate.combined385_part12 line 69
  29. def OAI.MUB6.TaoCertificate.combined385 line 71
  30. theorem OAI.MUB6.TaoCertificate.combined385_checked line 73
  31. theorem OAI.MUB6.TaoCertificate.combined385_zero line 76
  32. def OAI.MUB6.TaoCertificate.combined386_part0 line 84
  33. def OAI.MUB6.TaoCertificate.combined386_part1 line 86
  34. def OAI.MUB6.TaoCertificate.combined386_part2 line 88
  35. def OAI.MUB6.TaoCertificate.combined386_part3 line 90
  36. def OAI.MUB6.TaoCertificate.combined386_part4 line 92
  37. def OAI.MUB6.TaoCertificate.combined386_part5 line 94
  38. def OAI.MUB6.TaoCertificate.combined386_part6 line 96
  39. def OAI.MUB6.TaoCertificate.combined386_part7 line 98
  40. def OAI.MUB6.TaoCertificate.combined386_part8 line 100
  41. def OAI.MUB6.TaoCertificate.combined386_part9 line 102
  42. def OAI.MUB6.TaoCertificate.combined386_part10 line 104
  43. def OAI.MUB6.TaoCertificate.combined386_part11 line 106
  44. def OAI.MUB6.TaoCertificate.combined386_part12 line 108
  45. def OAI.MUB6.TaoCertificate.combined386 line 110
  46. theorem OAI.MUB6.TaoCertificate.combined386_checked line 112
  47. theorem OAI.MUB6.TaoCertificate.combined386_zero line 115
  48. def OAI.MUB6.TaoCertificate.combined387_part0 line 123
  49. def OAI.MUB6.TaoCertificate.combined387_part1 line 125
  50. def OAI.MUB6.TaoCertificate.combined387_part2 line 127
  51. def OAI.MUB6.TaoCertificate.combined387_part3 line 129
  52. def OAI.MUB6.TaoCertificate.combined387_part4 line 131
  53. def OAI.MUB6.TaoCertificate.combined387_part5 line 133
  54. def OAI.MUB6.TaoCertificate.combined387_part6 line 135
  55. def OAI.MUB6.TaoCertificate.combined387_part7 line 137
  56. def OAI.MUB6.TaoCertificate.combined387_part8 line 139
  57. def OAI.MUB6.TaoCertificate.combined387_part9 line 141
  58. def OAI.MUB6.TaoCertificate.combined387_part10 line 143
  59. def OAI.MUB6.TaoCertificate.combined387_part11 line 145
  60. def OAI.MUB6.TaoCertificate.combined387_part12 line 147
  61. def OAI.MUB6.TaoCertificate.combined387 line 149
  62. theorem OAI.MUB6.TaoCertificate.combined387_checked line 151
  63. theorem OAI.MUB6.TaoCertificate.combined387_zero line 154
  64. def OAI.MUB6.TaoCertificate.combined388_part0 line 162
  65. def OAI.MUB6.TaoCertificate.combined388_part1 line 164
  66. def OAI.MUB6.TaoCertificate.combined388_part2 line 166
  67. def OAI.MUB6.TaoCertificate.combined388_part3 line 168
  68. def OAI.MUB6.TaoCertificate.combined388_part4 line 170
  69. def OAI.MUB6.TaoCertificate.combined388_part5 line 172
  70. def OAI.MUB6.TaoCertificate.combined388_part6 line 174
  71. def OAI.MUB6.TaoCertificate.combined388_part7 line 176
  72. def OAI.MUB6.TaoCertificate.combined388_part8 line 178
  73. def OAI.MUB6.TaoCertificate.combined388_part9 line 180
  74. def OAI.MUB6.TaoCertificate.combined388_part10 line 182
  75. def OAI.MUB6.TaoCertificate.combined388_part11 line 184
  76. def OAI.MUB6.TaoCertificate.combined388_part12 line 186
  77. def OAI.MUB6.TaoCertificate.combined388 line 188
  78. theorem OAI.MUB6.TaoCertificate.combined388_checked line 190
  79. theorem OAI.MUB6.TaoCertificate.combined388_zero line 193
  80. def OAI.MUB6.TaoCertificate.combined389_part0 line 201
  81. def OAI.MUB6.TaoCertificate.combined389_part1 line 203
  82. def OAI.MUB6.TaoCertificate.combined389_part2 line 205
  83. def OAI.MUB6.TaoCertificate.combined389_part3 line 207
  84. def OAI.MUB6.TaoCertificate.combined389_part4 line 209
  85. def OAI.MUB6.TaoCertificate.combined389_part5 line 211
  86. def OAI.MUB6.TaoCertificate.combined389_part6 line 213
  87. def OAI.MUB6.TaoCertificate.combined389_part7 line 215
  88. def OAI.MUB6.TaoCertificate.combined389_part8 line 217
  89. def OAI.MUB6.TaoCertificate.combined389_part9 line 219
  90. def OAI.MUB6.TaoCertificate.combined389_part10 line 221
  91. def OAI.MUB6.TaoCertificate.combined389_part11 line 223
  92. def OAI.MUB6.TaoCertificate.combined389_part12 line 225
  93. def OAI.MUB6.TaoCertificate.combined389_part13 line 227
  94. def OAI.MUB6.TaoCertificate.combined389 line 229
  95. theorem OAI.MUB6.TaoCertificate.combined389_checked line 231
  96. theorem OAI.MUB6.TaoCertificate.combined389_zero line 234
  97. def OAI.MUB6.TaoCertificate.combined390_part0 line 242
  98. def OAI.MUB6.TaoCertificate.combined390_part1 line 244
  99. def OAI.MUB6.TaoCertificate.combined390_part2 line 246
  100. def OAI.MUB6.TaoCertificate.combined390_part3 line 248
  101. def OAI.MUB6.TaoCertificate.combined390_part4 line 250
  102. def OAI.MUB6.TaoCertificate.combined390_part5 line 252
  103. def OAI.MUB6.TaoCertificate.combined390_part6 line 254
  104. def OAI.MUB6.TaoCertificate.combined390_part7 line 256
  105. def OAI.MUB6.TaoCertificate.combined390_part8 line 258
  106. def OAI.MUB6.TaoCertificate.combined390_part9 line 260
  107. def OAI.MUB6.TaoCertificate.combined390_part10 line 262
  108. def OAI.MUB6.TaoCertificate.combined390_part11 line 264
  109. def OAI.MUB6.TaoCertificate.combined390_part12 line 266
  110. def OAI.MUB6.TaoCertificate.combined390_part13 line 268
  111. def OAI.MUB6.TaoCertificate.combined390 line 270
  112. theorem OAI.MUB6.TaoCertificate.combined390_checked line 272
  113. theorem OAI.MUB6.TaoCertificate.combined390_zero line 275
  114. def OAI.MUB6.TaoCertificate.combined391_part0 line 283
  115. def OAI.MUB6.TaoCertificate.combined391_part1 line 285
  116. def OAI.MUB6.TaoCertificate.combined391_part2 line 287
  117. def OAI.MUB6.TaoCertificate.combined391_part3 line 289
  118. def OAI.MUB6.TaoCertificate.combined391_part4 line 291
  119. def OAI.MUB6.TaoCertificate.combined391_part5 line 293
  120. def OAI.MUB6.TaoCertificate.combined391_part6 line 295
  121. def OAI.MUB6.TaoCertificate.combined391_part7 line 297
  122. def OAI.MUB6.TaoCertificate.combined391_part8 line 299
  123. def OAI.MUB6.TaoCertificate.combined391_part9 line 301
  124. def OAI.MUB6.TaoCertificate.combined391_part10 line 303
  125. def OAI.MUB6.TaoCertificate.combined391_part11 line 305
  126. def OAI.MUB6.TaoCertificate.combined391_part12 line 307
  127. def OAI.MUB6.TaoCertificate.combined391_part13 line 309
  128. def OAI.MUB6.TaoCertificate.combined391 line 311
  129. theorem OAI.MUB6.TaoCertificate.combined391_checked line 313
  130. theorem OAI.MUB6.TaoCertificate.combined391_zero line 316