OAI/Analysis/MutuallyUnbiased/PairMerge/Block2.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged64 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck64 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero64 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged65 line 19
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck65 line 21
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero65 line 23
  7. def OAI.MUB6.Certificate.PairData.pairMerged66 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck66 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero66 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged67 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck67 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero67 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged68 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck68 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero68 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged69 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck69 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero69 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged70 line 66
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck70 line 68
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero70 line 70
  22. def OAI.MUB6.Certificate.PairData.pairMerged71 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck71 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero71 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged72 line 85
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck72 line 87
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero72 line 89
  28. def OAI.MUB6.Certificate.PairData.pairMerged73 line 94
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck73 line 96
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero73 line 98
  31. def OAI.MUB6.Certificate.PairData.pairMerged74 line 103
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck74 line 105
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero74 line 107
  34. def OAI.MUB6.Certificate.PairData.pairMerged75 line 113
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck75 line 115
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero75 line 117
  37. def OAI.MUB6.Certificate.PairData.pairMerged76 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck76 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero76 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged77 line 133
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck77 line 135
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero77 line 137
  43. def OAI.MUB6.Certificate.PairData.pairMerged78 line 142
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck78 line 144
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero78 line 146
  46. def OAI.MUB6.Certificate.PairData.pairMerged79 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck79 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero79 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged80 line 161
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck80 line 163
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero80 line 165
  52. def OAI.MUB6.Certificate.PairData.pairMerged81 line 170
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck81 line 172
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero81 line 174
  55. def OAI.MUB6.Certificate.PairData.pairMerged82 line 179
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck82 line 181
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero82 line 183
  58. def OAI.MUB6.Certificate.PairData.pairMerged83 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck83 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero83 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged84 line 199
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck84 line 201
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero84 line 203
  64. def OAI.MUB6.Certificate.PairData.pairMerged85 line 208
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck85 line 210
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero85 line 212
  67. def OAI.MUB6.Certificate.PairData.pairMerged86 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck86 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero86 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged87 line 227
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck87 line 229
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero87 line 231
  73. def OAI.MUB6.Certificate.PairData.pairMerged88 line 236
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck88 line 238
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero88 line 240
  76. def OAI.MUB6.Certificate.PairData.pairMerged89 line 245
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck89 line 247
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero89 line 249
  79. def OAI.MUB6.Certificate.PairData.pairMerged90 line 255
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck90 line 257
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero90 line 259
  82. def OAI.MUB6.Certificate.PairData.pairMerged91 line 265
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck91 line 267
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero91 line 269
  85. def OAI.MUB6.Certificate.PairData.pairMerged92 line 275
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck92 line 277
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero92 line 279
  88. def OAI.MUB6.Certificate.PairData.pairMerged93 line 285
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck93 line 287
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero93 line 289
  91. def OAI.MUB6.Certificate.PairData.pairMerged94 line 294
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck94 line 296
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero94 line 298
  94. def OAI.MUB6.Certificate.PairData.pairMerged95 line 303
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck95 line 305
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero95 line 307