OAI/Analysis/MutuallyUnbiased/MixedMerge/Block0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged0 line 8
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck0 line 10
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero0 line 12
  4. def OAI.MUB6.Certificate.MixedData.merged1 line 17
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1 line 19
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1 line 21
  7. def OAI.MUB6.Certificate.MixedData.merged2 line 26
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2 line 28
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2 line 30
  10. def OAI.MUB6.Certificate.MixedData.merged3 line 36
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck3 line 38
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero3 line 40
  13. def OAI.MUB6.Certificate.MixedData.merged4 line 45
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck4 line 47
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero4 line 49
  16. def OAI.MUB6.Certificate.MixedData.merged5 line 54
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck5 line 56
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero5 line 58
  19. def OAI.MUB6.Certificate.MixedData.merged6 line 64
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck6 line 66
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero6 line 68
  22. def OAI.MUB6.Certificate.MixedData.merged7 line 74
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck7 line 76
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero7 line 78
  25. def OAI.MUB6.Certificate.MixedData.merged8 line 84
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck8 line 86
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero8 line 88
  28. def OAI.MUB6.Certificate.MixedData.merged9 line 93
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck9 line 95
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero9 line 97
  31. def OAI.MUB6.Certificate.MixedData.merged10 line 102
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck10 line 104
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero10 line 106
  34. def OAI.MUB6.Certificate.MixedData.merged11 line 112
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck11 line 114
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero11 line 116
  37. def OAI.MUB6.Certificate.MixedData.merged12 line 121
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck12 line 123
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero12 line 125
  40. def OAI.MUB6.Certificate.MixedData.merged13 line 130
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck13 line 132
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero13 line 134
  43. def OAI.MUB6.Certificate.MixedData.merged14 line 140
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck14 line 142
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero14 line 144
  46. def OAI.MUB6.Certificate.MixedData.merged15 line 150
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck15 line 152
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero15 line 154
  49. def OAI.MUB6.Certificate.MixedData.merged16 line 160
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck16 line 162
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero16 line 164
  52. def OAI.MUB6.Certificate.MixedData.merged17 line 170
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck17 line 172
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero17 line 174
  55. def OAI.MUB6.Certificate.MixedData.merged18 line 179
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck18 line 181
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero18 line 183
  58. def OAI.MUB6.Certificate.MixedData.merged19 line 188
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck19 line 190
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero19 line 192
  61. def OAI.MUB6.Certificate.MixedData.merged20 line 198
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck20 line 200
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero20 line 202
  64. def OAI.MUB6.Certificate.MixedData.merged21 line 207
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck21 line 209
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero21 line 211
  67. def OAI.MUB6.Certificate.MixedData.merged22 line 216
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck22 line 218
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero22 line 220
  70. def OAI.MUB6.Certificate.MixedData.merged23 line 226
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck23 line 228
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero23 line 230
  73. def OAI.MUB6.Certificate.MixedData.merged24 line 236
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck24 line 238
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero24 line 240
  76. def OAI.MUB6.Certificate.MixedData.merged25 line 246
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck25 line 248
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero25 line 250
  79. def OAI.MUB6.Certificate.MixedData.merged26 line 255
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck26 line 257
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero26 line 259
  82. def OAI.MUB6.Certificate.MixedData.merged27 line 264
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck27 line 266
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero27 line 268
  85. def OAI.MUB6.Certificate.MixedData.merged28 line 274
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck28 line 276
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero28 line 278
  88. def OAI.MUB6.Certificate.MixedData.merged29 line 284
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck29 line 286
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero29 line 288
  91. def OAI.MUB6.Certificate.MixedData.merged30 line 293
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck30 line 295
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero30 line 297
  94. def OAI.MUB6.Certificate.MixedData.merged31 line 302
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck31 line 304
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero31 line 306