OAI/Analysis/MutuallyUnbiased/PairMerge/Block0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged0 line 8
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck0 line 10
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero0 line 12
  4. def OAI.MUB6.Certificate.PairData.pairMerged1 line 17
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck1 line 19
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero1 line 21
  7. def OAI.MUB6.Certificate.PairData.pairMerged2 line 27
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck2 line 29
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero2 line 31
  10. def OAI.MUB6.Certificate.PairData.pairMerged3 line 36
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck3 line 38
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero3 line 40
  13. def OAI.MUB6.Certificate.PairData.pairMerged4 line 45
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck4 line 47
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero4 line 49
  16. def OAI.MUB6.Certificate.PairData.pairMerged5 line 55
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck5 line 57
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero5 line 59
  19. def OAI.MUB6.Certificate.PairData.pairMerged6 line 65
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck6 line 67
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero6 line 69
  22. def OAI.MUB6.Certificate.PairData.pairMerged7 line 74
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck7 line 76
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero7 line 78
  25. def OAI.MUB6.Certificate.PairData.pairMerged8 line 83
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck8 line 85
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero8 line 87
  28. def OAI.MUB6.Certificate.PairData.pairMerged9 line 93
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck9 line 95
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero9 line 97
  31. def OAI.MUB6.Certificate.PairData.pairMerged10 line 102
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck10 line 104
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero10 line 106
  34. def OAI.MUB6.Certificate.PairData.pairMerged11 line 111
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck11 line 113
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero11 line 115
  37. def OAI.MUB6.Certificate.PairData.pairMerged12 line 121
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck12 line 123
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero12 line 125
  40. def OAI.MUB6.Certificate.PairData.pairMerged13 line 131
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck13 line 133
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero13 line 135
  43. def OAI.MUB6.Certificate.PairData.pairMerged14 line 141
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck14 line 143
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero14 line 145
  46. def OAI.MUB6.Certificate.PairData.pairMerged15 line 150
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck15 line 152
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero15 line 154
  49. def OAI.MUB6.Certificate.PairData.pairMerged16 line 159
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck16 line 161
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero16 line 163
  52. def OAI.MUB6.Certificate.PairData.pairMerged17 line 169
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck17 line 171
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero17 line 173
  55. def OAI.MUB6.Certificate.PairData.pairMerged18 line 178
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck18 line 180
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero18 line 182
  58. def OAI.MUB6.Certificate.PairData.pairMerged19 line 187
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck19 line 189
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero19 line 191
  61. def OAI.MUB6.Certificate.PairData.pairMerged20 line 197
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck20 line 199
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero20 line 201
  64. def OAI.MUB6.Certificate.PairData.pairMerged21 line 207
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck21 line 209
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero21 line 211
  67. def OAI.MUB6.Certificate.PairData.pairMerged22 line 216
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck22 line 218
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero22 line 220
  70. def OAI.MUB6.Certificate.PairData.pairMerged23 line 225
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck23 line 227
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero23 line 229
  73. def OAI.MUB6.Certificate.PairData.pairMerged24 line 235
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck24 line 237
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero24 line 239
  76. def OAI.MUB6.Certificate.PairData.pairMerged25 line 244
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck25 line 246
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero25 line 248
  79. def OAI.MUB6.Certificate.PairData.pairMerged26 line 253
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck26 line 255
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero26 line 257
  82. def OAI.MUB6.Certificate.PairData.pairMerged27 line 263
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck27 line 265
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero27 line 267
  85. def OAI.MUB6.Certificate.PairData.pairMerged28 line 273
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck28 line 275
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero28 line 277
  88. def OAI.MUB6.Certificate.PairData.pairMerged29 line 283
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck29 line 285
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero29 line 287
  91. def OAI.MUB6.Certificate.PairData.pairMerged30 line 293
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck30 line 295
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero30 line 297
  94. def OAI.MUB6.Certificate.PairData.pairMerged31 line 302
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck31 line 304
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero31 line 306