OAI/Analysis/MutuallyUnbiased/MixedMerge/Block17.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged544 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck544 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero544 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged545 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck545 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero545 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged546 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck546 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero546 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged547 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck547 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero547 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged548 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck548 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero548 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged549 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck549 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero549 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged550 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck550 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero550 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged551 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck551 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero551 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged552 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck552 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero552 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged553 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck553 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero553 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged554 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck554 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero554 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged555 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck555 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero555 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged556 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck556 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero556 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged557 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck557 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero557 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged558 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck558 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero558 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged559 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck559 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero559 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged560 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck560 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero560 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged561 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck561 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero561 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged562 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck562 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero562 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged563 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck563 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero563 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged564 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck564 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero564 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged565 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck565 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero565 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged566 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck566 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero566 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged567 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck567 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero567 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged568 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck568 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero568 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged569 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck569 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero569 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged570 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck570 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero570 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged571 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck571 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero571 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged572 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck572 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero572 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged573 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck573 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero573 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged574 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck574 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero574 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged575 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck575 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero575 line 309