OAI/Analysis/MutuallyUnbiased/MixedMerge/Block32.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1024 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1024 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1024 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1025 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1025 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1025 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1026 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1026 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1026 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1027 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1027 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1027 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1028 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1028 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1028 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1029 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1029 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1029 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1030 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1030 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1030 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1031 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1031 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1031 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1032 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1032 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1032 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1033 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1033 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1033 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1034 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1034 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1034 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1035 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1035 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1035 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1036 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1036 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1036 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged1037 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1037 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1037 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1038 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1038 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1038 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1039 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1039 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1039 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1040 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1040 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1040 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1041 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1041 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1041 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1042 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1042 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1042 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1043 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1043 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1043 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1044 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1044 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1044 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1045 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1045 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1045 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1046 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1046 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1046 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1047 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1047 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1047 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1048 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1048 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1048 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1049 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1049 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1049 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1050 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1050 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1050 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1051 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1051 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1051 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1052 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1052 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1052 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1053 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1053 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1053 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1054 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1054 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1054 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged1055 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1055 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1055 line 311