OAI/Analysis/MutuallyUnbiased/PairMerge/Block10.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged320 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck320 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero320 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged321 line 19
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck321 line 21
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero321 line 23
  7. def OAI.MUB6.Certificate.PairData.pairMerged322 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck322 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero322 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged323 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck323 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero323 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged324 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck324 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero324 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged325 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck325 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero325 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged326 line 66
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck326 line 68
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero326 line 70
  22. def OAI.MUB6.Certificate.PairData.pairMerged327 line 76
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck327 line 78
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero327 line 80
  25. def OAI.MUB6.Certificate.PairData.pairMerged328 line 85
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck328 line 87
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero328 line 89
  28. def OAI.MUB6.Certificate.PairData.pairMerged329 line 94
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck329 line 96
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero329 line 98
  31. def OAI.MUB6.Certificate.PairData.pairMerged330 line 104
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck330 line 106
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero330 line 108
  34. def OAI.MUB6.Certificate.PairData.pairMerged331 line 114
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck331 line 116
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero331 line 118
  37. def OAI.MUB6.Certificate.PairData.pairMerged332 line 124
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck332 line 126
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero332 line 128
  40. def OAI.MUB6.Certificate.PairData.pairMerged333 line 134
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck333 line 136
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero333 line 138
  43. def OAI.MUB6.Certificate.PairData.pairMerged334 line 143
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck334 line 145
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero334 line 147
  46. def OAI.MUB6.Certificate.PairData.pairMerged335 line 153
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck335 line 155
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero335 line 157
  49. def OAI.MUB6.Certificate.PairData.pairMerged336 line 162
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck336 line 164
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero336 line 166
  52. def OAI.MUB6.Certificate.PairData.pairMerged337 line 172
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck337 line 174
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero337 line 176
  55. def OAI.MUB6.Certificate.PairData.pairMerged338 line 182
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck338 line 184
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero338 line 186
  58. def OAI.MUB6.Certificate.PairData.pairMerged339 line 191
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck339 line 193
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero339 line 195
  61. def OAI.MUB6.Certificate.PairData.pairMerged340 line 201
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck340 line 203
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero340 line 205
  64. def OAI.MUB6.Certificate.PairData.pairMerged341 line 210
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck341 line 212
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero341 line 214
  67. def OAI.MUB6.Certificate.PairData.pairMerged342 line 219
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck342 line 221
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero342 line 223
  70. def OAI.MUB6.Certificate.PairData.pairMerged343 line 229
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck343 line 231
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero343 line 233
  73. def OAI.MUB6.Certificate.PairData.pairMerged344 line 239
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck344 line 241
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero344 line 243
  76. def OAI.MUB6.Certificate.PairData.pairMerged345 line 249
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck345 line 251
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero345 line 253
  79. def OAI.MUB6.Certificate.PairData.pairMerged346 line 258
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck346 line 260
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero346 line 262
  82. def OAI.MUB6.Certificate.PairData.pairMerged347 line 268
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck347 line 270
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero347 line 272
  85. def OAI.MUB6.Certificate.PairData.pairMerged348 line 277
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck348 line 279
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero348 line 281
  88. def OAI.MUB6.Certificate.PairData.pairMerged349 line 286
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck349 line 288
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero349 line 290
  91. def OAI.MUB6.Certificate.PairData.pairMerged350 line 296
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck350 line 298
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero350 line 300
  94. def OAI.MUB6.Certificate.PairData.pairMerged351 line 306
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck351 line 308
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero351 line 310