OAI/Analysis/MutuallyUnbiased/MixedMerge/Block30.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged960 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck960 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero960 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged961 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck961 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero961 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged962 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck962 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero962 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged963 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck963 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero963 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged964 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck964 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero964 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged965 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck965 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero965 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged966 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck966 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero966 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged967 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck967 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero967 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged968 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck968 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero968 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged969 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck969 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero969 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged970 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck970 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero970 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged971 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck971 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero971 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged972 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck972 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero972 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged973 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck973 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero973 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged974 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck974 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero974 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged975 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck975 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero975 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged976 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck976 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero976 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged977 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck977 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero977 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged978 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck978 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero978 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged979 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck979 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero979 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged980part0 line 201
  62. def OAI.MUB6.Certificate.MixedData.merged980part1 line 203
  63. def OAI.MUB6.Certificate.MixedData.merged980part2 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged980part3 line 207
  65. def OAI.MUB6.Certificate.MixedData.merged980part4 line 209
  66. def OAI.MUB6.Certificate.MixedData.merged980part5 line 211
  67. def OAI.MUB6.Certificate.MixedData.merged980part6 line 213
  68. def OAI.MUB6.Certificate.MixedData.merged980part7 line 215
  69. def OAI.MUB6.Certificate.MixedData.merged980 line 217
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck980 line 219
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero980 line 221
  72. def OAI.MUB6.Certificate.MixedData.merged981 line 227
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck981 line 229
  74. theorem OAI.MUB6.Certificate.MixedData.mergedZero981 line 231
  75. def OAI.MUB6.Certificate.MixedData.merged982 line 236
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck982 line 238
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero982 line 240
  78. def OAI.MUB6.Certificate.MixedData.merged983 line 245
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck983 line 247
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero983 line 249
  81. def OAI.MUB6.Certificate.MixedData.merged984 line 255
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck984 line 257
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero984 line 259
  84. def OAI.MUB6.Certificate.MixedData.merged985 line 264
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck985 line 266
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero985 line 268
  87. def OAI.MUB6.Certificate.MixedData.merged986 line 273
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck986 line 275
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero986 line 277
  90. def OAI.MUB6.Certificate.MixedData.merged987 line 283
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck987 line 285
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero987 line 287
  93. def OAI.MUB6.Certificate.MixedData.merged988 line 293
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck988 line 295
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero988 line 297
  96. def OAI.MUB6.Certificate.MixedData.merged989 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck989 line 305
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero989 line 307
  99. def OAI.MUB6.Certificate.MixedData.merged990 line 312
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck990 line 314
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero990 line 316
  102. def OAI.MUB6.Certificate.MixedData.merged991 line 321
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck991 line 323
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero991 line 325