OAI/Analysis/MutuallyUnbiased/MixedMerge/Block10.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged320 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck320 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero320 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged321 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck321 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero321 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged322 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck322 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero322 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged323 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck323 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero323 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged324 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck324 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero324 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged325 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck325 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero325 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged326 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck326 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero326 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged327 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck327 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero327 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged328 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck328 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero328 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged329 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck329 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero329 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged330 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck330 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero330 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged331 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck331 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero331 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged332 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck332 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero332 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged333 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck333 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero333 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged334 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck334 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero334 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged335 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck335 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero335 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged336 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck336 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero336 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged337 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck337 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero337 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged338 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck338 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero338 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged339 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck339 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero339 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged340 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck340 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero340 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged341 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck341 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero341 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged342 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck342 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero342 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged343 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck343 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero343 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged344 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck344 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero344 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged345 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck345 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero345 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged346 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck346 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero346 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged347 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck347 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero347 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged348 line 276
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck348 line 278
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero348 line 280
  88. def OAI.MUB6.Certificate.MixedData.merged349 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck349 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero349 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged350 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck350 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero350 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged351 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck351 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero351 line 309