OAI/Analysis/MutuallyUnbiased/MixedMerge/Block22.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged704 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck704 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero704 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged705 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck705 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero705 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged706 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck706 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero706 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged707 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck707 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero707 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged708 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck708 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero708 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged709 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck709 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero709 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged710 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck710 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero710 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged711 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck711 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero711 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged712 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck712 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero712 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged713 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck713 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero713 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged714 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck714 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero714 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged715 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck715 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero715 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged716 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck716 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero716 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged717 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck717 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero717 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged718 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck718 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero718 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged719 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck719 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero719 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged720 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck720 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero720 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged721 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck721 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero721 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged722 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck722 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero722 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged723 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck723 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero723 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged724 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck724 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero724 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged725 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck725 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero725 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged726 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck726 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero726 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged727 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck727 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero727 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged728 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck728 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero728 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged729 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck729 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero729 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged730 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck730 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero730 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged731 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck731 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero731 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged732 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck732 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero732 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged733 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck733 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero733 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged734 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck734 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero734 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged735 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck735 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero735 line 310