OAI/Analysis/MutuallyUnbiased/PairMerge/Block8.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged256 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck256 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero256 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged257 line 18
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck257 line 20
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero257 line 22
  7. def OAI.MUB6.Certificate.PairData.pairMerged258 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck258 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero258 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged259 line 38
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck259 line 40
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero259 line 42
  13. def OAI.MUB6.Certificate.PairData.pairMerged260 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck260 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero260 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged261 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck261 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero261 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged262 line 66
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck262 line 68
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero262 line 70
  22. def OAI.MUB6.Certificate.PairData.pairMerged263 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck263 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero263 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged264 line 85
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck264 line 87
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero264 line 89
  28. def OAI.MUB6.Certificate.PairData.pairMerged265 line 95
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck265 line 97
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero265 line 99
  31. def OAI.MUB6.Certificate.PairData.pairMerged266 line 105
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck266 line 107
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero266 line 109
  34. def OAI.MUB6.Certificate.PairData.pairMerged267 line 114
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck267 line 116
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero267 line 118
  37. def OAI.MUB6.Certificate.PairData.pairMerged268 line 124
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck268 line 126
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero268 line 128
  40. def OAI.MUB6.Certificate.PairData.pairMerged269 line 133
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck269 line 135
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero269 line 137
  43. def OAI.MUB6.Certificate.PairData.pairMerged270 line 142
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck270 line 144
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero270 line 146
  46. def OAI.MUB6.Certificate.PairData.pairMerged271 line 152
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck271 line 154
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero271 line 156
  49. def OAI.MUB6.Certificate.PairData.pairMerged272 line 162
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck272 line 164
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero272 line 166
  52. def OAI.MUB6.Certificate.PairData.pairMerged273 line 171
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck273 line 173
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero273 line 175
  55. def OAI.MUB6.Certificate.PairData.pairMerged274 line 181
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck274 line 183
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero274 line 185
  58. def OAI.MUB6.Certificate.PairData.pairMerged275 line 190
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck275 line 192
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero275 line 194
  61. def OAI.MUB6.Certificate.PairData.pairMerged276 line 199
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck276 line 201
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero276 line 203
  64. def OAI.MUB6.Certificate.PairData.pairMerged277 line 209
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck277 line 211
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero277 line 213
  67. def OAI.MUB6.Certificate.PairData.pairMerged278 line 219
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck278 line 221
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero278 line 223
  70. def OAI.MUB6.Certificate.PairData.pairMerged279 line 229
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck279 line 231
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero279 line 233
  73. def OAI.MUB6.Certificate.PairData.pairMerged280 line 239
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck280 line 241
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero280 line 243
  76. def OAI.MUB6.Certificate.PairData.pairMerged281 line 248
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck281 line 250
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero281 line 252
  79. def OAI.MUB6.Certificate.PairData.pairMerged282 line 258
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck282 line 260
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero282 line 262
  82. def OAI.MUB6.Certificate.PairData.pairMerged283 line 267
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck283 line 269
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero283 line 271
  85. def OAI.MUB6.Certificate.PairData.pairMerged284 line 277
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck284 line 279
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero284 line 281
  88. def OAI.MUB6.Certificate.PairData.pairMerged285 line 287
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck285 line 289
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero285 line 291
  91. def OAI.MUB6.Certificate.PairData.pairMerged286 line 296
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck286 line 298
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero286 line 300
  94. def OAI.MUB6.Certificate.PairData.pairMerged287 line 306
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck287 line 308
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero287 line 310