OAI/Analysis/MutuallyUnbiased/MixedMerge/Block21.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged672 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck672 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero672 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged673 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck673 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero673 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged674 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck674 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero674 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged675 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck675 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero675 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged676 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck676 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero676 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged677 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck677 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero677 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged678part0 line 68
  20. def OAI.MUB6.Certificate.MixedData.merged678part1 line 70
  21. def OAI.MUB6.Certificate.MixedData.merged678part2 line 72
  22. def OAI.MUB6.Certificate.MixedData.merged678part3 line 74
  23. def OAI.MUB6.Certificate.MixedData.merged678part4 line 76
  24. def OAI.MUB6.Certificate.MixedData.merged678part5 line 78
  25. def OAI.MUB6.Certificate.MixedData.merged678part6 line 80
  26. def OAI.MUB6.Certificate.MixedData.merged678part7 line 82
  27. def OAI.MUB6.Certificate.MixedData.merged678 line 84
  28. theorem OAI.MUB6.Certificate.MixedData.mergeCheck678 line 86
  29. theorem OAI.MUB6.Certificate.MixedData.mergedZero678 line 88
  30. def OAI.MUB6.Certificate.MixedData.merged679 line 94
  31. theorem OAI.MUB6.Certificate.MixedData.mergeCheck679 line 96
  32. theorem OAI.MUB6.Certificate.MixedData.mergedZero679 line 98
  33. def OAI.MUB6.Certificate.MixedData.merged680 line 103
  34. theorem OAI.MUB6.Certificate.MixedData.mergeCheck680 line 105
  35. theorem OAI.MUB6.Certificate.MixedData.mergedZero680 line 107
  36. def OAI.MUB6.Certificate.MixedData.merged681 line 112
  37. theorem OAI.MUB6.Certificate.MixedData.mergeCheck681 line 114
  38. theorem OAI.MUB6.Certificate.MixedData.mergedZero681 line 116
  39. def OAI.MUB6.Certificate.MixedData.merged682 line 122
  40. theorem OAI.MUB6.Certificate.MixedData.mergeCheck682 line 124
  41. theorem OAI.MUB6.Certificate.MixedData.mergedZero682 line 126
  42. def OAI.MUB6.Certificate.MixedData.merged683 line 131
  43. theorem OAI.MUB6.Certificate.MixedData.mergeCheck683 line 133
  44. theorem OAI.MUB6.Certificate.MixedData.mergedZero683 line 135
  45. def OAI.MUB6.Certificate.MixedData.merged684 line 140
  46. theorem OAI.MUB6.Certificate.MixedData.mergeCheck684 line 142
  47. theorem OAI.MUB6.Certificate.MixedData.mergedZero684 line 144
  48. def OAI.MUB6.Certificate.MixedData.merged685 line 150
  49. theorem OAI.MUB6.Certificate.MixedData.mergeCheck685 line 152
  50. theorem OAI.MUB6.Certificate.MixedData.mergedZero685 line 154
  51. def OAI.MUB6.Certificate.MixedData.merged686 line 160
  52. theorem OAI.MUB6.Certificate.MixedData.mergeCheck686 line 162
  53. theorem OAI.MUB6.Certificate.MixedData.mergedZero686 line 164
  54. def OAI.MUB6.Certificate.MixedData.merged687 line 170
  55. theorem OAI.MUB6.Certificate.MixedData.mergeCheck687 line 172
  56. theorem OAI.MUB6.Certificate.MixedData.mergedZero687 line 174
  57. def OAI.MUB6.Certificate.MixedData.merged688 line 179
  58. theorem OAI.MUB6.Certificate.MixedData.mergeCheck688 line 181
  59. theorem OAI.MUB6.Certificate.MixedData.mergedZero688 line 183
  60. def OAI.MUB6.Certificate.MixedData.merged689 line 188
  61. theorem OAI.MUB6.Certificate.MixedData.mergeCheck689 line 190
  62. theorem OAI.MUB6.Certificate.MixedData.mergedZero689 line 192
  63. def OAI.MUB6.Certificate.MixedData.merged690 line 198
  64. theorem OAI.MUB6.Certificate.MixedData.mergeCheck690 line 200
  65. theorem OAI.MUB6.Certificate.MixedData.mergedZero690 line 202
  66. def OAI.MUB6.Certificate.MixedData.merged691 line 208
  67. theorem OAI.MUB6.Certificate.MixedData.mergeCheck691 line 210
  68. theorem OAI.MUB6.Certificate.MixedData.mergedZero691 line 212
  69. def OAI.MUB6.Certificate.MixedData.merged692 line 217
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck692 line 219
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero692 line 221
  72. def OAI.MUB6.Certificate.MixedData.merged693 line 226
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck693 line 228
  74. theorem OAI.MUB6.Certificate.MixedData.mergedZero693 line 230
  75. def OAI.MUB6.Certificate.MixedData.merged694 line 236
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck694 line 238
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero694 line 240
  78. def OAI.MUB6.Certificate.MixedData.merged695 line 246
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck695 line 248
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero695 line 250
  81. def OAI.MUB6.Certificate.MixedData.merged696 line 256
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck696 line 258
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero696 line 260
  84. def OAI.MUB6.Certificate.MixedData.merged697 line 266
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck697 line 268
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero697 line 270
  87. def OAI.MUB6.Certificate.MixedData.merged698 line 275
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck698 line 277
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero698 line 279
  90. def OAI.MUB6.Certificate.MixedData.merged699 line 284
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck699 line 286
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero699 line 288
  93. def OAI.MUB6.Certificate.MixedData.merged700 line 294
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck700 line 296
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero700 line 298
  96. def OAI.MUB6.Certificate.MixedData.merged701 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck701 line 305
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero701 line 307
  99. def OAI.MUB6.Certificate.MixedData.merged702 line 312
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck702 line 314
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero702 line 316
  102. def OAI.MUB6.Certificate.MixedData.merged703 line 322
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck703 line 324
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero703 line 326