OAI/Analysis/MutuallyUnbiased/PairMerge/Block3.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged96 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck96 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero96 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged97 line 18
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck97 line 20
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero97 line 22
  7. def OAI.MUB6.Certificate.PairData.pairMerged98 line 27
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck98 line 29
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero98 line 31
  10. def OAI.MUB6.Certificate.PairData.pairMerged99 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck99 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero99 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged100 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck100 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero100 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged101 line 56
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck101 line 58
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero101 line 60
  19. def OAI.MUB6.Certificate.PairData.pairMerged102 line 65
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck102 line 67
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero102 line 69
  22. def OAI.MUB6.Certificate.PairData.pairMerged103 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck103 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero103 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged104 line 84
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck104 line 86
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero104 line 88
  28. def OAI.MUB6.Certificate.PairData.pairMerged105 line 93
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck105 line 95
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero105 line 97
  31. def OAI.MUB6.Certificate.PairData.pairMerged106 line 103
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck106 line 105
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero106 line 107
  34. def OAI.MUB6.Certificate.PairData.pairMerged107 line 113
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck107 line 115
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero107 line 117
  37. def OAI.MUB6.Certificate.PairData.pairMerged108 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck108 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero108 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged109 line 132
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck109 line 134
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero109 line 136
  43. def OAI.MUB6.Certificate.PairData.pairMerged110 line 141
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck110 line 143
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero110 line 145
  46. def OAI.MUB6.Certificate.PairData.pairMerged111 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck111 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero111 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged112 line 160
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck112 line 162
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero112 line 164
  52. def OAI.MUB6.Certificate.PairData.pairMerged113 line 169
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck113 line 171
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero113 line 173
  55. def OAI.MUB6.Certificate.PairData.pairMerged114 line 179
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck114 line 181
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero114 line 183
  58. def OAI.MUB6.Certificate.PairData.pairMerged115 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck115 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero115 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged116 line 198
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck116 line 200
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero116 line 202
  64. def OAI.MUB6.Certificate.PairData.pairMerged117 line 207
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck117 line 209
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero117 line 211
  67. def OAI.MUB6.Certificate.PairData.pairMerged118 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck118 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero118 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged119 line 226
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck119 line 228
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero119 line 230
  73. def OAI.MUB6.Certificate.PairData.pairMerged120 line 235
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck120 line 237
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero120 line 239
  76. def OAI.MUB6.Certificate.PairData.pairMerged121 line 245
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck121 line 247
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero121 line 249
  79. def OAI.MUB6.Certificate.PairData.pairMerged122 line 255
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck122 line 257
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero122 line 259
  82. def OAI.MUB6.Certificate.PairData.pairMerged123 line 265
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck123 line 267
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero123 line 269
  85. def OAI.MUB6.Certificate.PairData.pairMerged124 line 275
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck124 line 277
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero124 line 279
  88. def OAI.MUB6.Certificate.PairData.pairMerged125 line 285
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck125 line 287
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero125 line 289
  91. def OAI.MUB6.Certificate.PairData.pairMerged126 line 295
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck126 line 297
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero126 line 299
  94. def OAI.MUB6.Certificate.PairData.pairMerged127 line 304
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck127 line 306
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero127 line 308