OAI/Analysis/MutuallyUnbiased/MixedTargets/OriginalMerge5.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80part0 line 13
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80part1 line 15
  3. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80part2 line 17
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80part3 line 19
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80part4 line 21
  6. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80part5 line 23
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80 line 25
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode80 line 27
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode80Check line 29
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval80 line 31
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode81 line 37
  12. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode81 line 39
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode81Check line 41
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval81 line 43
  15. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode82 line 49
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode82 line 51
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode82Check line 53
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval82 line 55
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode83 line 61
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode83 line 63
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode83Check line 65
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval83 line 67
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode84 line 73
  24. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode84 line 75
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode84Check line 77
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval84 line 79
  27. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85part0 line 85
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85part1 line 87
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85part2 line 89
  30. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85part3 line 91
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85part4 line 93
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85 line 95
  33. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode85 line 97
  34. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode85Check line 99
  35. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval85 line 101
  36. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part0 line 107
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part1 line 109
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part2 line 111
  39. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part3 line 113
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part4 line 115
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part5 line 117
  42. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part6 line 119
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part7 line 121
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86part8 line 123
  45. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86 line 125
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode86 line 127
  47. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode86Check line 129
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval86 line 131
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part0 line 137
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part1 line 139
  51. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part2 line 141
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part3 line 143
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part4 line 145
  54. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part5 line 147
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part6 line 149
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part7 line 151
  57. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part8 line 153
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part9 line 155
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part10 line 157
  60. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part11 line 159
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87part12 line 161
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87 line 163
  63. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode87 line 165
  64. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode87Check line 167
  65. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval87 line 169
  66. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part0 line 175
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part1 line 177
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part2 line 179
  69. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part3 line 181
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part4 line 183
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part5 line 185
  72. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part6 line 187
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part7 line 189
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part8 line 191
  75. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part9 line 193
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part10 line 195
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part11 line 197
  78. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part12 line 199
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part13 line 201
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part14 line 203
  81. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part15 line 205
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part16 line 207
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part17 line 209
  84. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part18 line 211
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88part19 line 213
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88 line 215
  87. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode88 line 217
  88. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode88Check line 219
  89. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval88 line 221
  90. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part0 line 227
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part1 line 229
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part2 line 231
  93. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part3 line 233
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part4 line 235
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part5 line 237
  96. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part6 line 239
  97. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part7 line 241
  98. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part8 line 243
  99. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part9 line 245
  100. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part10 line 247
  101. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part11 line 249
  102. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part12 line 251
  103. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part13 line 253
  104. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part14 line 255
  105. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part15 line 257
  106. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part16 line 259
  107. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part17 line 261
  108. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part18 line 263
  109. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part19 line 265
  110. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part20 line 267
  111. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part21 line 269
  112. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part22 line 271
  113. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part23 line 273
  114. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part24 line 275
  115. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part25 line 277
  116. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part26 line 279
  117. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part27 line 281
  118. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part28 line 283
  119. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89part29 line 285
  120. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89 line 287
  121. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode89 line 289
  122. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode89Check line 291
  123. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval89 line 293