OAI/Analysis/MutuallyUnbiased/PairMerge/Block9.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged288 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck288 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero288 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged289 line 18
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck289 line 20
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero289 line 22
  7. def OAI.MUB6.Certificate.PairData.pairMerged290 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck290 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero290 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged291 line 38
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck291 line 40
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero291 line 42
  13. def OAI.MUB6.Certificate.PairData.pairMerged292 line 48
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck292 line 50
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero292 line 52
  16. def OAI.MUB6.Certificate.PairData.pairMerged293 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck293 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero293 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged294 line 67
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck294 line 69
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero294 line 71
  22. def OAI.MUB6.Certificate.PairData.pairMerged295 line 76
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck295 line 78
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero295 line 80
  25. def OAI.MUB6.Certificate.PairData.pairMerged296 line 85
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck296 line 87
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero296 line 89
  28. def OAI.MUB6.Certificate.PairData.pairMerged297 line 95
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck297 line 97
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero297 line 99
  31. def OAI.MUB6.Certificate.PairData.pairMerged298 line 105
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck298 line 107
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero298 line 109
  34. def OAI.MUB6.Certificate.PairData.pairMerged299 line 114
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck299 line 116
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero299 line 118
  37. def OAI.MUB6.Certificate.PairData.pairMerged300 line 124
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck300 line 126
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero300 line 128
  40. def OAI.MUB6.Certificate.PairData.pairMerged301 line 133
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck301 line 135
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero301 line 137
  43. def OAI.MUB6.Certificate.PairData.pairMerged302 line 142
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck302 line 144
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero302 line 146
  46. def OAI.MUB6.Certificate.PairData.pairMerged303 line 152
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck303 line 154
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero303 line 156
  49. def OAI.MUB6.Certificate.PairData.pairMerged304 line 162
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck304 line 164
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero304 line 166
  52. def OAI.MUB6.Certificate.PairData.pairMerged305 line 172
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck305 line 174
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero305 line 176
  55. def OAI.MUB6.Certificate.PairData.pairMerged306 line 182
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck306 line 184
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero306 line 186
  58. def OAI.MUB6.Certificate.PairData.pairMerged307 line 192
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck307 line 194
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero307 line 196
  61. def OAI.MUB6.Certificate.PairData.pairMerged308 line 201
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck308 line 203
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero308 line 205
  64. def OAI.MUB6.Certificate.PairData.pairMerged309 line 211
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck309 line 213
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero309 line 215
  67. def OAI.MUB6.Certificate.PairData.pairMerged310 line 220
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck310 line 222
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero310 line 224
  70. def OAI.MUB6.Certificate.PairData.pairMerged311 line 230
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck311 line 232
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero311 line 234
  73. def OAI.MUB6.Certificate.PairData.pairMerged312 line 240
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck312 line 242
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero312 line 244
  76. def OAI.MUB6.Certificate.PairData.pairMerged313 line 249
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck313 line 251
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero313 line 253
  79. def OAI.MUB6.Certificate.PairData.pairMerged314 line 259
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck314 line 261
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero314 line 263
  82. def OAI.MUB6.Certificate.PairData.pairMerged315 line 268
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck315 line 270
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero315 line 272
  85. def OAI.MUB6.Certificate.PairData.pairMerged316 line 277
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck316 line 279
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero316 line 281
  88. def OAI.MUB6.Certificate.PairData.pairMerged317 line 287
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck317 line 289
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero317 line 291
  91. def OAI.MUB6.Certificate.PairData.pairMerged318 line 297
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck318 line 299
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero318 line 301
  94. def OAI.MUB6.Certificate.PairData.pairMerged319 line 307
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck319 line 309
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero319 line 311