OAI/Analysis/MutuallyUnbiased/PairMerge/Block6.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged192 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck192 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero192 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged193 line 18
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck193 line 20
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero193 line 22
  7. def OAI.MUB6.Certificate.PairData.pairMerged194 line 27
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck194 line 29
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero194 line 31
  10. def OAI.MUB6.Certificate.PairData.pairMerged195 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck195 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero195 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged196 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck196 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero196 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged197 line 56
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck197 line 58
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero197 line 60
  19. def OAI.MUB6.Certificate.PairData.pairMerged198 line 65
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck198 line 67
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero198 line 69
  22. def OAI.MUB6.Certificate.PairData.pairMerged199 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck199 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero199 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged200 line 84
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck200 line 86
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero200 line 88
  28. def OAI.MUB6.Certificate.PairData.pairMerged201 line 93
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck201 line 95
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero201 line 97
  31. def OAI.MUB6.Certificate.PairData.pairMerged202 line 103
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck202 line 105
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero202 line 107
  34. def OAI.MUB6.Certificate.PairData.pairMerged203 line 113
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck203 line 115
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero203 line 117
  37. def OAI.MUB6.Certificate.PairData.pairMerged204 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck204 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero204 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged205 line 132
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck205 line 134
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero205 line 136
  43. def OAI.MUB6.Certificate.PairData.pairMerged206 line 141
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck206 line 143
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero206 line 145
  46. def OAI.MUB6.Certificate.PairData.pairMerged207 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck207 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero207 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged208 line 160
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck208 line 162
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero208 line 164
  52. def OAI.MUB6.Certificate.PairData.pairMerged209 line 169
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck209 line 171
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero209 line 173
  55. def OAI.MUB6.Certificate.PairData.pairMerged210 line 179
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck210 line 181
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero210 line 183
  58. def OAI.MUB6.Certificate.PairData.pairMerged211 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck211 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero211 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged212 line 198
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck212 line 200
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero212 line 202
  64. def OAI.MUB6.Certificate.PairData.pairMerged213 line 207
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck213 line 209
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero213 line 211
  67. def OAI.MUB6.Certificate.PairData.pairMerged214 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck214 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero214 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged215 line 226
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck215 line 228
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero215 line 230
  73. def OAI.MUB6.Certificate.PairData.pairMerged216 line 235
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck216 line 237
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero216 line 239
  76. def OAI.MUB6.Certificate.PairData.pairMerged217 line 245
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck217 line 247
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero217 line 249
  79. def OAI.MUB6.Certificate.PairData.pairMerged218 line 255
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck218 line 257
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero218 line 259
  82. def OAI.MUB6.Certificate.PairData.pairMerged219 line 265
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck219 line 267
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero219 line 269
  85. def OAI.MUB6.Certificate.PairData.pairMerged220 line 275
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck220 line 277
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero220 line 279
  88. def OAI.MUB6.Certificate.PairData.pairMerged221 line 284
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck221 line 286
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero221 line 288
  91. def OAI.MUB6.Certificate.PairData.pairMerged222 line 293
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck222 line 295
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero222 line 297
  94. def OAI.MUB6.Certificate.PairData.pairMerged223 line 303
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck223 line 305
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero223 line 307