OAI/Analysis/MutuallyUnbiased/PairMerge/Block4.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged128 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck128 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero128 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged129 line 19
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck129 line 21
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero129 line 23
  7. def OAI.MUB6.Certificate.PairData.pairMerged130 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck130 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero130 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged131 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck131 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero131 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged132 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck132 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero132 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged133 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck133 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero133 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged134 line 66
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck134 line 68
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero134 line 70
  22. def OAI.MUB6.Certificate.PairData.pairMerged135 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck135 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero135 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged136 line 85
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck136 line 87
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero136 line 89
  28. def OAI.MUB6.Certificate.PairData.pairMerged137 line 94
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck137 line 96
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero137 line 98
  31. def OAI.MUB6.Certificate.PairData.pairMerged138 line 103
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck138 line 105
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero138 line 107
  34. def OAI.MUB6.Certificate.PairData.pairMerged139 line 113
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck139 line 115
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero139 line 117
  37. def OAI.MUB6.Certificate.PairData.pairMerged140 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck140 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero140 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged141 line 133
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck141 line 135
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero141 line 137
  43. def OAI.MUB6.Certificate.PairData.pairMerged142 line 142
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck142 line 144
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero142 line 146
  46. def OAI.MUB6.Certificate.PairData.pairMerged143 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck143 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero143 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged144 line 161
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck144 line 163
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero144 line 165
  52. def OAI.MUB6.Certificate.PairData.pairMerged145 line 170
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck145 line 172
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero145 line 174
  55. def OAI.MUB6.Certificate.PairData.pairMerged146 line 179
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck146 line 181
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero146 line 183
  58. def OAI.MUB6.Certificate.PairData.pairMerged147 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck147 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero147 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged148 line 199
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck148 line 201
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero148 line 203
  64. def OAI.MUB6.Certificate.PairData.pairMerged149 line 208
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck149 line 210
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero149 line 212
  67. def OAI.MUB6.Certificate.PairData.pairMerged150 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck150 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero150 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged151 line 227
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck151 line 229
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero151 line 231
  73. def OAI.MUB6.Certificate.PairData.pairMerged152 line 236
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck152 line 238
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero152 line 240
  76. def OAI.MUB6.Certificate.PairData.pairMerged153 line 245
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck153 line 247
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero153 line 249
  79. def OAI.MUB6.Certificate.PairData.pairMerged154 line 255
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck154 line 257
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero154 line 259
  82. def OAI.MUB6.Certificate.PairData.pairMerged155 line 265
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck155 line 267
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero155 line 269
  85. def OAI.MUB6.Certificate.PairData.pairMerged156 line 275
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck156 line 277
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero156 line 279
  88. def OAI.MUB6.Certificate.PairData.pairMerged157 line 285
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck157 line 287
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero157 line 289
  91. def OAI.MUB6.Certificate.PairData.pairMerged158 line 294
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck158 line 296
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero158 line 298
  94. def OAI.MUB6.Certificate.PairData.pairMerged159 line 303
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck159 line 305
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero159 line 307