OAI/Analysis/MutuallyUnbiased/MixedMerge/Block33.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1056part0 line 9
  2. def OAI.MUB6.Certificate.MixedData.merged1056part1 line 11
  3. def OAI.MUB6.Certificate.MixedData.merged1056part2 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1056part3 line 15
  5. def OAI.MUB6.Certificate.MixedData.merged1056part4 line 17
  6. def OAI.MUB6.Certificate.MixedData.merged1056part5 line 19
  7. def OAI.MUB6.Certificate.MixedData.merged1056part6 line 21
  8. def OAI.MUB6.Certificate.MixedData.merged1056part7 line 23
  9. def OAI.MUB6.Certificate.MixedData.merged1056part8 line 25
  10. def OAI.MUB6.Certificate.MixedData.merged1056part9 line 27
  11. def OAI.MUB6.Certificate.MixedData.merged1056part10 line 29
  12. def OAI.MUB6.Certificate.MixedData.merged1056 line 31
  13. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1056 line 33
  14. theorem OAI.MUB6.Certificate.MixedData.mergedZero1056 line 35
  15. def OAI.MUB6.Certificate.MixedData.merged1057 line 41
  16. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1057 line 43
  17. theorem OAI.MUB6.Certificate.MixedData.mergedZero1057 line 45
  18. def OAI.MUB6.Certificate.MixedData.merged1058 line 50
  19. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1058 line 52
  20. theorem OAI.MUB6.Certificate.MixedData.mergedZero1058 line 54
  21. def OAI.MUB6.Certificate.MixedData.merged1059 line 59
  22. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1059 line 61
  23. theorem OAI.MUB6.Certificate.MixedData.mergedZero1059 line 63
  24. def OAI.MUB6.Certificate.MixedData.merged1060 line 69
  25. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1060 line 71
  26. theorem OAI.MUB6.Certificate.MixedData.mergedZero1060 line 73
  27. def OAI.MUB6.Certificate.MixedData.merged1061 line 78
  28. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1061 line 80
  29. theorem OAI.MUB6.Certificate.MixedData.mergedZero1061 line 82
  30. def OAI.MUB6.Certificate.MixedData.merged1062 line 87
  31. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1062 line 89
  32. theorem OAI.MUB6.Certificate.MixedData.mergedZero1062 line 91
  33. def OAI.MUB6.Certificate.MixedData.merged1063 line 97
  34. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1063 line 99
  35. theorem OAI.MUB6.Certificate.MixedData.mergedZero1063 line 101
  36. def OAI.MUB6.Certificate.MixedData.merged1064 line 107
  37. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1064 line 109
  38. theorem OAI.MUB6.Certificate.MixedData.mergedZero1064 line 111
  39. def OAI.MUB6.Certificate.MixedData.merged1065 line 117
  40. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1065 line 119
  41. theorem OAI.MUB6.Certificate.MixedData.mergedZero1065 line 121
  42. def OAI.MUB6.Certificate.MixedData.merged1066 line 126
  43. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1066 line 128
  44. theorem OAI.MUB6.Certificate.MixedData.mergedZero1066 line 130
  45. def OAI.MUB6.Certificate.MixedData.merged1067 line 135
  46. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1067 line 137
  47. theorem OAI.MUB6.Certificate.MixedData.mergedZero1067 line 139
  48. def OAI.MUB6.Certificate.MixedData.merged1068 line 145
  49. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1068 line 147
  50. theorem OAI.MUB6.Certificate.MixedData.mergedZero1068 line 149
  51. def OAI.MUB6.Certificate.MixedData.merged1069 line 155
  52. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1069 line 157
  53. theorem OAI.MUB6.Certificate.MixedData.mergedZero1069 line 159
  54. def OAI.MUB6.Certificate.MixedData.merged1070 line 164
  55. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1070 line 166
  56. theorem OAI.MUB6.Certificate.MixedData.mergedZero1070 line 168
  57. def OAI.MUB6.Certificate.MixedData.merged1071 line 173
  58. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1071 line 175
  59. theorem OAI.MUB6.Certificate.MixedData.mergedZero1071 line 177
  60. def OAI.MUB6.Certificate.MixedData.merged1072 line 183
  61. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1072 line 185
  62. theorem OAI.MUB6.Certificate.MixedData.mergedZero1072 line 187
  63. def OAI.MUB6.Certificate.MixedData.merged1073 line 193
  64. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1073 line 195
  65. theorem OAI.MUB6.Certificate.MixedData.mergedZero1073 line 197
  66. def OAI.MUB6.Certificate.MixedData.merged1074 line 203
  67. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1074 line 205
  68. theorem OAI.MUB6.Certificate.MixedData.mergedZero1074 line 207
  69. def OAI.MUB6.Certificate.MixedData.merged1075 line 213
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1075 line 215
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero1075 line 217
  72. def OAI.MUB6.Certificate.MixedData.merged1076 line 222
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1076 line 224
  74. theorem OAI.MUB6.Certificate.MixedData.mergedZero1076 line 226
  75. def OAI.MUB6.Certificate.MixedData.merged1077 line 231
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1077 line 233
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero1077 line 235
  78. def OAI.MUB6.Certificate.MixedData.merged1078 line 241
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1078 line 243
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero1078 line 245
  81. def OAI.MUB6.Certificate.MixedData.merged1079 line 250
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1079 line 252
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero1079 line 254
  84. def OAI.MUB6.Certificate.MixedData.merged1080 line 259
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1080 line 261
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero1080 line 263
  87. def OAI.MUB6.Certificate.MixedData.merged1081 line 269
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1081 line 271
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero1081 line 273
  90. def OAI.MUB6.Certificate.MixedData.merged1082 line 279
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1082 line 281
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero1082 line 283
  93. def OAI.MUB6.Certificate.MixedData.merged1083 line 289
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1083 line 291
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero1083 line 293
  96. def OAI.MUB6.Certificate.MixedData.merged1084 line 298
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1084 line 300
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero1084 line 302
  99. def OAI.MUB6.Certificate.MixedData.merged1085 line 307
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1085 line 309
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero1085 line 311
  102. def OAI.MUB6.Certificate.MixedData.merged1086 line 317
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1086 line 319
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero1086 line 321
  105. def OAI.MUB6.Certificate.MixedData.merged1087 line 327
  106. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1087 line 329
  107. theorem OAI.MUB6.Certificate.MixedData.mergedZero1087 line 331