OAI/Analysis/MutuallyUnbiased/PairMerge/Block1.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged32 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck32 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero32 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged33 line 19
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck33 line 21
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero33 line 23
  7. def OAI.MUB6.Certificate.PairData.pairMerged34 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck34 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero34 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged35 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck35 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero35 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged36 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck36 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero36 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged37 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck37 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero37 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged38 line 66
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck38 line 68
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero38 line 70
  22. def OAI.MUB6.Certificate.PairData.pairMerged39 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck39 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero39 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged40 line 85
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck40 line 87
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero40 line 89
  28. def OAI.MUB6.Certificate.PairData.pairMerged41 line 94
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck41 line 96
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero41 line 98
  31. def OAI.MUB6.Certificate.PairData.pairMerged42 line 103
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck42 line 105
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero42 line 107
  34. def OAI.MUB6.Certificate.PairData.pairMerged43 line 113
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck43 line 115
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero43 line 117
  37. def OAI.MUB6.Certificate.PairData.pairMerged44 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck44 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero44 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged45 line 133
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck45 line 135
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero45 line 137
  43. def OAI.MUB6.Certificate.PairData.pairMerged46 line 142
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck46 line 144
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero46 line 146
  46. def OAI.MUB6.Certificate.PairData.pairMerged47 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck47 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero47 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged48 line 161
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck48 line 163
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero48 line 165
  52. def OAI.MUB6.Certificate.PairData.pairMerged49 line 170
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck49 line 172
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero49 line 174
  55. def OAI.MUB6.Certificate.PairData.pairMerged50 line 179
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck50 line 181
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero50 line 183
  58. def OAI.MUB6.Certificate.PairData.pairMerged51 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck51 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero51 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged52 line 199
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck52 line 201
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero52 line 203
  64. def OAI.MUB6.Certificate.PairData.pairMerged53 line 208
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck53 line 210
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero53 line 212
  67. def OAI.MUB6.Certificate.PairData.pairMerged54 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck54 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero54 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged55 line 227
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck55 line 229
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero55 line 231
  73. def OAI.MUB6.Certificate.PairData.pairMerged56 line 236
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck56 line 238
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero56 line 240
  76. def OAI.MUB6.Certificate.PairData.pairMerged57 line 245
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck57 line 247
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero57 line 249
  79. def OAI.MUB6.Certificate.PairData.pairMerged58 line 255
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck58 line 257
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero58 line 259
  82. def OAI.MUB6.Certificate.PairData.pairMerged59 line 265
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck59 line 267
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero59 line 269
  85. def OAI.MUB6.Certificate.PairData.pairMerged60 line 275
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck60 line 277
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero60 line 279
  88. def OAI.MUB6.Certificate.PairData.pairMerged61 line 285
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck61 line 287
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero61 line 289
  91. def OAI.MUB6.Certificate.PairData.pairMerged62 line 295
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck62 line 297
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero62 line 299
  94. def OAI.MUB6.Certificate.PairData.pairMerged63 line 304
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck63 line 306
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero63 line 308