OAI/Analysis/MutuallyUnbiased/MixedMerge/Block25.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged800 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck800 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero800 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged801 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck801 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero801 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged802 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck802 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero802 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged803 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck803 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero803 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged804 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck804 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero804 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged805 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck805 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero805 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged806 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck806 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero806 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged807 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck807 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero807 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged808 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck808 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero808 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged809 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck809 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero809 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged810 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck810 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero810 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged811 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck811 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero811 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged812 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck812 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero812 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged813 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck813 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero813 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged814 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck814 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero814 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged815 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck815 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero815 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged816 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck816 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero816 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged817 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck817 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero817 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged818 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck818 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero818 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged819 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck819 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero819 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged820 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck820 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero820 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged821 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck821 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero821 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged822 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck822 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero822 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged823 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck823 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero823 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged824 line 237
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck824 line 239
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero824 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged825 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck825 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero825 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged826 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck826 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero826 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged827 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck827 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero827 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged828 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck828 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero828 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged829part0 line 287
  89. def OAI.MUB6.Certificate.MixedData.merged829part1 line 289
  90. def OAI.MUB6.Certificate.MixedData.merged829part2 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged829part3 line 293
  92. def OAI.MUB6.Certificate.MixedData.merged829part4 line 295
  93. def OAI.MUB6.Certificate.MixedData.merged829part5 line 297
  94. def OAI.MUB6.Certificate.MixedData.merged829part6 line 299
  95. def OAI.MUB6.Certificate.MixedData.merged829part7 line 301
  96. def OAI.MUB6.Certificate.MixedData.merged829 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck829 line 305
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero829 line 307
  99. def OAI.MUB6.Certificate.MixedData.merged830 line 313
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck830 line 315
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero830 line 317
  102. def OAI.MUB6.Certificate.MixedData.merged831 line 322
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck831 line 324
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero831 line 326