OAI/Analysis/MutuallyUnbiased/MixedMerge/Block27.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged864 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck864 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero864 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged865 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck865 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero865 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged866 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck866 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero866 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged867 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck867 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero867 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged868 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck868 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero868 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged869 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck869 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero869 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged870 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck870 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero870 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged871 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck871 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero871 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged872 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck872 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero872 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged873 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck873 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero873 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged874 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck874 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero874 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged875 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck875 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero875 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged876 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck876 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero876 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged877 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck877 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero877 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged878 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck878 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero878 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged879 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck879 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero879 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged880 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck880 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero880 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged881 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck881 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero881 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged882 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck882 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero882 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged883 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck883 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero883 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged884 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck884 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero884 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged885 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck885 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero885 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged886 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck886 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero886 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged887 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck887 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero887 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged888 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck888 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero888 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged889 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck889 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero889 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged890 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck890 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero890 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged891 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck891 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero891 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged892 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck892 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero892 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged893 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck893 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero893 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged894 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck894 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero894 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged895 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck895 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero895 line 309