OAI/Analysis/MutuallyUnbiased/MixedTargets/OriginalMerge2.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode32 line 22
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode32 line 24
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode32Check line 26
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval32 line 28
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode33 line 34
  6. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode33 line 36
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode33Check line 38
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval33 line 40
  9. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode34 line 46
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode34 line 48
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode34Check line 50
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval34 line 52
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode35 line 58
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode35 line 60
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode35Check line 62
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval35 line 64
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode36 line 70
  18. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode36 line 72
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode36Check line 74
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval36 line 76
  21. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode37 line 82
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode37 line 84
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode37Check line 86
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval37 line 88
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode38 line 94
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode38 line 96
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode38Check line 98
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval38 line 100
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode39 line 106
  30. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode39 line 108
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode39Check line 110
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval39 line 112
  33. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode40 line 118
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode40 line 120
  35. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode40Check line 122
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval40 line 124
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41part0 line 130
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41part1 line 132
  39. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41part2 line 134
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41part3 line 136
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41part4 line 138
  42. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41 line 140
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode41 line 142
  44. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode41Check line 144
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval41 line 146
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part0 line 152
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part1 line 154
  48. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part2 line 156
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part3 line 158
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part4 line 160
  51. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part5 line 162
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part6 line 164
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part7 line 166
  54. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42part8 line 168
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42 line 170
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode42 line 172
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode42Check line 174
  58. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval42 line 176
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part0 line 182
  60. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part1 line 184
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part2 line 186
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part3 line 188
  63. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part4 line 190
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part5 line 192
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part6 line 194
  66. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part7 line 196
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part8 line 198
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part9 line 200
  69. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part10 line 202
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part11 line 204
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part12 line 206
  72. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43part13 line 208
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43 line 210
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode43 line 212
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode43Check line 214
  76. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval43 line 216
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode44 line 222
  78. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode44 line 224
  79. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode44Check line 226
  80. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval44 line 228
  81. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode45 line 234
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode45 line 236
  83. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode45Check line 238
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval45 line 240
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode46 line 246
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode46 line 248
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode46Check line 250
  88. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval46 line 252
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode47 line 258
  90. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode47 line 260
  91. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode47Check line 262
  92. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval47 line 264