OAI/Analysis/MutuallyUnbiased/MixedMerge/Block31.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged992 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck992 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero992 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged993 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck993 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero993 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged994 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck994 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero994 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged995 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck995 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero995 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged996 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck996 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero996 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged997 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck997 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero997 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged998 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck998 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero998 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged999 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck999 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero999 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged1000 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1000 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1000 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1001 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1001 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1001 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1002 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1002 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1002 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1003 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1003 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1003 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1004 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1004 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1004 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1005 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1005 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1005 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1006 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1006 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1006 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1007 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1007 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1007 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1008 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1008 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1008 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1009 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1009 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1009 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1010 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1010 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1010 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1011 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1011 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1011 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1012 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1012 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1012 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1013 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1013 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1013 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1014 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1014 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1014 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1015 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1015 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1015 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1016 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1016 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1016 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1017 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1017 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1017 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1018 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1018 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1018 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged1019 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1019 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1019 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1020 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1020 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1020 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1021 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1021 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1021 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1022 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1022 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1022 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1023 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1023 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1023 line 309