OAI/Analysis/MutuallyUnbiased/MixedMerge/Block34.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1088 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1088 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1088 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1089 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1089 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1089 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1090 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1090 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1090 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1091 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1091 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1091 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1092 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1092 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1092 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1093 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1093 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1093 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged1094 line 68
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1094 line 70
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1094 line 72
  22. def OAI.MUB6.Certificate.MixedData.merged1095 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1095 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1095 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged1096 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1096 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1096 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1097 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1097 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1097 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged1098 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1098 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1098 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1099 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1099 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1099 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1100 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1100 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1100 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1101 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1101 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1101 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1102 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1102 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1102 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged1103 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1103 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1103 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1104 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1104 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1104 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1105 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1105 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1105 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1106 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1106 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1106 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged1107 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1107 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1107 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1108 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1108 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1108 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1109 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1109 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1109 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1110 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1110 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1110 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1111 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1111 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1111 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged1112 line 240
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1112 line 242
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1112 line 244
  76. def OAI.MUB6.Certificate.MixedData.merged1113 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1113 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1113 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1114 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1114 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1114 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1115 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1115 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1115 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1116 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1116 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1116 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1117 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1117 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1117 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1118 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1118 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1118 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1119 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1119 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1119 line 310