OAI/Analysis/MutuallyUnbiased/MixedMerge/Block3.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged96 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck96 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero96 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged97 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck97 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero97 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged98 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck98 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero98 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged99 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck99 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero99 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged100 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck100 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero100 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged101 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck101 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero101 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged102 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck102 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero102 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged103 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck103 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero103 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged104 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck104 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero104 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged105 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck105 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero105 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged106 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck106 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero106 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged107 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck107 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero107 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged108 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck108 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero108 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged109 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck109 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero109 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged110 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck110 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero110 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged111 line 154
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck111 line 156
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero111 line 158
  49. def OAI.MUB6.Certificate.MixedData.merged112 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck112 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero112 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged113 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck113 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero113 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged114 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck114 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero114 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged115 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck115 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero115 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged116 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck116 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero116 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged117 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck117 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero117 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged118 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck118 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero118 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged119 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck119 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero119 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged120 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck120 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero120 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged121 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck121 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero121 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged122 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck122 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero122 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged123 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck123 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero123 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged124 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck124 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero124 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged125 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck125 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero125 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged126 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck126 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero126 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged127 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck127 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero127 line 310