OAI/Analysis/MutuallyUnbiased/PairMerge/Block5.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged160 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck160 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero160 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged161 line 18
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck161 line 20
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero161 line 22
  7. def OAI.MUB6.Certificate.PairData.pairMerged162 line 27
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck162 line 29
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero162 line 31
  10. def OAI.MUB6.Certificate.PairData.pairMerged163 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck163 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero163 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged164 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck164 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero164 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged165 line 56
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck165 line 58
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero165 line 60
  19. def OAI.MUB6.Certificate.PairData.pairMerged166 line 65
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck166 line 67
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero166 line 69
  22. def OAI.MUB6.Certificate.PairData.pairMerged167 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck167 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero167 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged168 line 84
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck168 line 86
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero168 line 88
  28. def OAI.MUB6.Certificate.PairData.pairMerged169 line 93
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck169 line 95
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero169 line 97
  31. def OAI.MUB6.Certificate.PairData.pairMerged170 line 103
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck170 line 105
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero170 line 107
  34. def OAI.MUB6.Certificate.PairData.pairMerged171 line 113
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck171 line 115
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero171 line 117
  37. def OAI.MUB6.Certificate.PairData.pairMerged172 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck172 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero172 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged173 line 132
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck173 line 134
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero173 line 136
  43. def OAI.MUB6.Certificate.PairData.pairMerged174 line 141
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck174 line 143
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero174 line 145
  46. def OAI.MUB6.Certificate.PairData.pairMerged175 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck175 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero175 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged176 line 160
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck176 line 162
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero176 line 164
  52. def OAI.MUB6.Certificate.PairData.pairMerged177 line 169
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck177 line 171
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero177 line 173
  55. def OAI.MUB6.Certificate.PairData.pairMerged178 line 179
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck178 line 181
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero178 line 183
  58. def OAI.MUB6.Certificate.PairData.pairMerged179 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck179 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero179 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged180 line 198
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck180 line 200
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero180 line 202
  64. def OAI.MUB6.Certificate.PairData.pairMerged181 line 207
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck181 line 209
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero181 line 211
  67. def OAI.MUB6.Certificate.PairData.pairMerged182 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck182 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero182 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged183 line 226
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck183 line 228
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero183 line 230
  73. def OAI.MUB6.Certificate.PairData.pairMerged184 line 235
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck184 line 237
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero184 line 239
  76. def OAI.MUB6.Certificate.PairData.pairMerged185 line 245
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck185 line 247
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero185 line 249
  79. def OAI.MUB6.Certificate.PairData.pairMerged186 line 255
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck186 line 257
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero186 line 259
  82. def OAI.MUB6.Certificate.PairData.pairMerged187 line 265
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck187 line 267
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero187 line 269
  85. def OAI.MUB6.Certificate.PairData.pairMerged188 line 275
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck188 line 277
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero188 line 279
  88. def OAI.MUB6.Certificate.PairData.pairMerged189 line 285
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck189 line 287
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero189 line 289
  91. def OAI.MUB6.Certificate.PairData.pairMerged190 line 294
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck190 line 296
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero190 line 298
  94. def OAI.MUB6.Certificate.PairData.pairMerged191 line 303
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck191 line 305
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero191 line 307