OAI/Analysis/MutuallyUnbiased/MixedMerge/Block29.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged928 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck928 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero928 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged929 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck929 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero929 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged930 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck930 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero930 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged931 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck931 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero931 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged932 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck932 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero932 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged933 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck933 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero933 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged934 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck934 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero934 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged935 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck935 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero935 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged936 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck936 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero936 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged937 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck937 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero937 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged938 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck938 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero938 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged939 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck939 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero939 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged940 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck940 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero940 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged941 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck941 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero941 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged942 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck942 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero942 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged943 line 154
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck943 line 156
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero943 line 158
  49. def OAI.MUB6.Certificate.MixedData.merged944 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck944 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero944 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged945 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck945 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero945 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged946 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck946 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero946 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged947 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck947 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero947 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged948 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck948 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero948 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged949 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck949 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero949 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged950 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck950 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero950 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged951 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck951 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero951 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged952 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck952 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero952 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged953 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck953 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero953 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged954 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck954 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero954 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged955 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck955 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero955 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged956 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck956 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero956 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged957 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck957 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero957 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged958 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck958 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero958 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged959 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck959 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero959 line 310