OAI/Analysis/MutuallyUnbiased/MixedMerge/Block12.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged384 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck384 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero384 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged385 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck385 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero385 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged386 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck386 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero386 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged387 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck387 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero387 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged388 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck388 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero388 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged389 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck389 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero389 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged390 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck390 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero390 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged391 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck391 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero391 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged392 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck392 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero392 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged393 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck393 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero393 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged394 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck394 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero394 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged395 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck395 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero395 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged396 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck396 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero396 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged397 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck397 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero397 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged398 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck398 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero398 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged399 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck399 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero399 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged400 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck400 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero400 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged401 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck401 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero401 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged402 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck402 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero402 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged403 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck403 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero403 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged404 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck404 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero404 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged405 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck405 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero405 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged406 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck406 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero406 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged407 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck407 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero407 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged408 line 237
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck408 line 239
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero408 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged409 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck409 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero409 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged410 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck410 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero410 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged411 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck411 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero411 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged412 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck412 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero412 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged413 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck413 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero413 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged414 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck414 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero414 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged415 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck415 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero415 line 309