OAI/Analysis/MutuallyUnbiased/MixedMerge/Block53.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1696 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1696 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1696 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1697 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1697 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1697 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1698 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1698 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1698 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1699part0 line 39
  11. def OAI.MUB6.Certificate.MixedData.merged1699part1 line 41
  12. def OAI.MUB6.Certificate.MixedData.merged1699part2 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged1699part3 line 45
  14. def OAI.MUB6.Certificate.MixedData.merged1699part4 line 47
  15. def OAI.MUB6.Certificate.MixedData.merged1699part5 line 49
  16. def OAI.MUB6.Certificate.MixedData.merged1699part6 line 51
  17. def OAI.MUB6.Certificate.MixedData.merged1699 line 53
  18. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1699 line 55
  19. theorem OAI.MUB6.Certificate.MixedData.mergedZero1699 line 57
  20. def OAI.MUB6.Certificate.MixedData.merged1700 line 63
  21. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1700 line 65
  22. theorem OAI.MUB6.Certificate.MixedData.mergedZero1700 line 67
  23. def OAI.MUB6.Certificate.MixedData.merged1701 line 72
  24. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1701 line 74
  25. theorem OAI.MUB6.Certificate.MixedData.mergedZero1701 line 76
  26. def OAI.MUB6.Certificate.MixedData.merged1702 line 81
  27. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1702 line 83
  28. theorem OAI.MUB6.Certificate.MixedData.mergedZero1702 line 85
  29. def OAI.MUB6.Certificate.MixedData.merged1703 line 91
  30. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1703 line 93
  31. theorem OAI.MUB6.Certificate.MixedData.mergedZero1703 line 95
  32. def OAI.MUB6.Certificate.MixedData.merged1704 line 100
  33. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1704 line 102
  34. theorem OAI.MUB6.Certificate.MixedData.mergedZero1704 line 104
  35. def OAI.MUB6.Certificate.MixedData.merged1705 line 109
  36. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1705 line 111
  37. theorem OAI.MUB6.Certificate.MixedData.mergedZero1705 line 113
  38. def OAI.MUB6.Certificate.MixedData.merged1706 line 119
  39. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1706 line 121
  40. theorem OAI.MUB6.Certificate.MixedData.mergedZero1706 line 123
  41. def OAI.MUB6.Certificate.MixedData.merged1707 line 129
  42. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1707 line 131
  43. theorem OAI.MUB6.Certificate.MixedData.mergedZero1707 line 133
  44. def OAI.MUB6.Certificate.MixedData.merged1708 line 139
  45. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1708 line 141
  46. theorem OAI.MUB6.Certificate.MixedData.mergedZero1708 line 143
  47. def OAI.MUB6.Certificate.MixedData.merged1709 line 148
  48. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1709 line 150
  49. theorem OAI.MUB6.Certificate.MixedData.mergedZero1709 line 152
  50. def OAI.MUB6.Certificate.MixedData.merged1710 line 157
  51. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1710 line 159
  52. theorem OAI.MUB6.Certificate.MixedData.mergedZero1710 line 161
  53. def OAI.MUB6.Certificate.MixedData.merged1711 line 167
  54. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1711 line 169
  55. theorem OAI.MUB6.Certificate.MixedData.mergedZero1711 line 171
  56. def OAI.MUB6.Certificate.MixedData.merged1712 line 177
  57. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1712 line 179
  58. theorem OAI.MUB6.Certificate.MixedData.mergedZero1712 line 181
  59. def OAI.MUB6.Certificate.MixedData.merged1713 line 186
  60. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1713 line 188
  61. theorem OAI.MUB6.Certificate.MixedData.mergedZero1713 line 190
  62. def OAI.MUB6.Certificate.MixedData.merged1714 line 195
  63. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1714 line 197
  64. theorem OAI.MUB6.Certificate.MixedData.mergedZero1714 line 199
  65. def OAI.MUB6.Certificate.MixedData.merged1715 line 205
  66. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1715 line 207
  67. theorem OAI.MUB6.Certificate.MixedData.mergedZero1715 line 209
  68. def OAI.MUB6.Certificate.MixedData.merged1716 line 215
  69. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1716 line 217
  70. theorem OAI.MUB6.Certificate.MixedData.mergedZero1716 line 219
  71. def OAI.MUB6.Certificate.MixedData.merged1717 line 225
  72. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1717 line 227
  73. theorem OAI.MUB6.Certificate.MixedData.mergedZero1717 line 229
  74. def OAI.MUB6.Certificate.MixedData.merged1718 line 235
  75. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1718 line 237
  76. theorem OAI.MUB6.Certificate.MixedData.mergedZero1718 line 239
  77. def OAI.MUB6.Certificate.MixedData.merged1719 line 244
  78. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1719 line 246
  79. theorem OAI.MUB6.Certificate.MixedData.mergedZero1719 line 248
  80. def OAI.MUB6.Certificate.MixedData.merged1720 line 253
  81. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1720 line 255
  82. theorem OAI.MUB6.Certificate.MixedData.mergedZero1720 line 257
  83. def OAI.MUB6.Certificate.MixedData.merged1721 line 263
  84. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1721 line 265
  85. theorem OAI.MUB6.Certificate.MixedData.mergedZero1721 line 267
  86. def OAI.MUB6.Certificate.MixedData.merged1722 line 272
  87. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1722 line 274
  88. theorem OAI.MUB6.Certificate.MixedData.mergedZero1722 line 276
  89. def OAI.MUB6.Certificate.MixedData.merged1723 line 281
  90. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1723 line 283
  91. theorem OAI.MUB6.Certificate.MixedData.mergedZero1723 line 285
  92. def OAI.MUB6.Certificate.MixedData.merged1724 line 291
  93. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1724 line 293
  94. theorem OAI.MUB6.Certificate.MixedData.mergedZero1724 line 295
  95. def OAI.MUB6.Certificate.MixedData.merged1725 line 301
  96. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1725 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergedZero1725 line 305
  98. def OAI.MUB6.Certificate.MixedData.merged1726 line 311
  99. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1726 line 313
  100. theorem OAI.MUB6.Certificate.MixedData.mergedZero1726 line 315
  101. def OAI.MUB6.Certificate.MixedData.merged1727 line 320
  102. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1727 line 322
  103. theorem OAI.MUB6.Certificate.MixedData.mergedZero1727 line 324