OAI/Analysis/MutuallyUnbiased/PairMerge/Block7.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged224 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck224 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero224 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged225 line 18
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck225 line 20
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero225 line 22
  7. def OAI.MUB6.Certificate.PairData.pairMerged226 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck226 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero226 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged227 line 38
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck227 line 40
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero227 line 42
  13. def OAI.MUB6.Certificate.PairData.pairMerged228 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck228 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero228 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged229 line 56
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck229 line 58
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero229 line 60
  19. def OAI.MUB6.Certificate.PairData.pairMerged230 line 66
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck230 line 68
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero230 line 70
  22. def OAI.MUB6.Certificate.PairData.pairMerged231 line 75
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck231 line 77
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero231 line 79
  25. def OAI.MUB6.Certificate.PairData.pairMerged232 line 84
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck232 line 86
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero232 line 88
  28. def OAI.MUB6.Certificate.PairData.pairMerged233 line 94
  29. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck233 line 96
  30. theorem OAI.MUB6.Certificate.PairData.pairMergedZero233 line 98
  31. def OAI.MUB6.Certificate.PairData.pairMerged234 line 104
  32. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck234 line 106
  33. theorem OAI.MUB6.Certificate.PairData.pairMergedZero234 line 108
  34. def OAI.MUB6.Certificate.PairData.pairMerged235 line 114
  35. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck235 line 116
  36. theorem OAI.MUB6.Certificate.PairData.pairMergedZero235 line 118
  37. def OAI.MUB6.Certificate.PairData.pairMerged236 line 123
  38. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck236 line 125
  39. theorem OAI.MUB6.Certificate.PairData.pairMergedZero236 line 127
  40. def OAI.MUB6.Certificate.PairData.pairMerged237 line 132
  41. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck237 line 134
  42. theorem OAI.MUB6.Certificate.PairData.pairMergedZero237 line 136
  43. def OAI.MUB6.Certificate.PairData.pairMerged238 line 142
  44. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck238 line 144
  45. theorem OAI.MUB6.Certificate.PairData.pairMergedZero238 line 146
  46. def OAI.MUB6.Certificate.PairData.pairMerged239 line 151
  47. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck239 line 153
  48. theorem OAI.MUB6.Certificate.PairData.pairMergedZero239 line 155
  49. def OAI.MUB6.Certificate.PairData.pairMerged240 line 160
  50. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck240 line 162
  51. theorem OAI.MUB6.Certificate.PairData.pairMergedZero240 line 164
  52. def OAI.MUB6.Certificate.PairData.pairMerged241 line 170
  53. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck241 line 172
  54. theorem OAI.MUB6.Certificate.PairData.pairMergedZero241 line 174
  55. def OAI.MUB6.Certificate.PairData.pairMerged242 line 180
  56. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck242 line 182
  57. theorem OAI.MUB6.Certificate.PairData.pairMergedZero242 line 184
  58. def OAI.MUB6.Certificate.PairData.pairMerged243 line 189
  59. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck243 line 191
  60. theorem OAI.MUB6.Certificate.PairData.pairMergedZero243 line 193
  61. def OAI.MUB6.Certificate.PairData.pairMerged244 line 198
  62. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck244 line 200
  63. theorem OAI.MUB6.Certificate.PairData.pairMergedZero244 line 202
  64. def OAI.MUB6.Certificate.PairData.pairMerged245 line 208
  65. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck245 line 210
  66. theorem OAI.MUB6.Certificate.PairData.pairMergedZero245 line 212
  67. def OAI.MUB6.Certificate.PairData.pairMerged246 line 217
  68. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck246 line 219
  69. theorem OAI.MUB6.Certificate.PairData.pairMergedZero246 line 221
  70. def OAI.MUB6.Certificate.PairData.pairMerged247 line 226
  71. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck247 line 228
  72. theorem OAI.MUB6.Certificate.PairData.pairMergedZero247 line 230
  73. def OAI.MUB6.Certificate.PairData.pairMerged248 line 236
  74. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck248 line 238
  75. theorem OAI.MUB6.Certificate.PairData.pairMergedZero248 line 240
  76. def OAI.MUB6.Certificate.PairData.pairMerged249 line 246
  77. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck249 line 248
  78. theorem OAI.MUB6.Certificate.PairData.pairMergedZero249 line 250
  79. def OAI.MUB6.Certificate.PairData.pairMerged250 line 256
  80. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck250 line 258
  81. theorem OAI.MUB6.Certificate.PairData.pairMergedZero250 line 260
  82. def OAI.MUB6.Certificate.PairData.pairMerged251 line 266
  83. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck251 line 268
  84. theorem OAI.MUB6.Certificate.PairData.pairMergedZero251 line 270
  85. def OAI.MUB6.Certificate.PairData.pairMerged252 line 276
  86. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck252 line 278
  87. theorem OAI.MUB6.Certificate.PairData.pairMergedZero252 line 280
  88. def OAI.MUB6.Certificate.PairData.pairMerged253 line 286
  89. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck253 line 288
  90. theorem OAI.MUB6.Certificate.PairData.pairMergedZero253 line 290
  91. def OAI.MUB6.Certificate.PairData.pairMerged254 line 296
  92. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck254 line 298
  93. theorem OAI.MUB6.Certificate.PairData.pairMergedZero254 line 300
  94. def OAI.MUB6.Certificate.PairData.pairMerged255 line 305
  95. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck255 line 307
  96. theorem OAI.MUB6.Certificate.PairData.pairMergedZero255 line 309