OAI/Analysis/MutuallyUnbiased/MixedMerge/Block2.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged64 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck64 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero64 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged65 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck65 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero65 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged66 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck66 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero66 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged67 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck67 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero67 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged68 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck68 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero68 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged69 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck69 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero69 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged70 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck70 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero70 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged71 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck71 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero71 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged72 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck72 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero72 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged73 line 97
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck73 line 99
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero73 line 101
  31. def OAI.MUB6.Certificate.MixedData.merged74 line 107
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck74 line 109
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero74 line 111
  34. def OAI.MUB6.Certificate.MixedData.merged75 line 116
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck75 line 118
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero75 line 120
  37. def OAI.MUB6.Certificate.MixedData.merged76 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck76 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero76 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged77 line 135
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck77 line 137
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero77 line 139
  43. def OAI.MUB6.Certificate.MixedData.merged78 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck78 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero78 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged79 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck79 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero79 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged80 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck80 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero80 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged81 line 173
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck81 line 175
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero81 line 177
  55. def OAI.MUB6.Certificate.MixedData.merged82 line 183
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck82 line 185
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero82 line 187
  58. def OAI.MUB6.Certificate.MixedData.merged83 line 192
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck83 line 194
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero83 line 196
  61. def OAI.MUB6.Certificate.MixedData.merged84 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck84 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero84 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged85 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck85 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero85 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged86 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck86 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero86 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged87 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck87 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero87 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged88 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck88 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero88 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged89 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck89 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero89 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged90 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck90 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero90 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged91 line 269
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck91 line 271
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero91 line 273
  85. def OAI.MUB6.Certificate.MixedData.merged92 line 279
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck92 line 281
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero92 line 283
  88. def OAI.MUB6.Certificate.MixedData.merged93 line 288
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck93 line 290
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero93 line 292
  91. def OAI.MUB6.Certificate.MixedData.merged94 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck94 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero94 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged95 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck95 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero95 line 311