OAI/Analysis/MutuallyUnbiased/MixedTargets/OriginalMerge1.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode16 line 23
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode16 line 25
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode16Check line 27
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval16 line 29
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode17 line 35
  6. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode17 line 37
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode17Check line 39
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval17 line 41
  9. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode18 line 47
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode18 line 49
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode18Check line 51
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval18 line 53
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19part0 line 59
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19part1 line 61
  15. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19part2 line 63
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19part3 line 65
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19part4 line 67
  18. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19 line 69
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode19 line 71
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode19Check line 73
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval19 line 75
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part0 line 81
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part1 line 83
  24. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part2 line 85
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part3 line 87
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part4 line 89
  27. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part5 line 91
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20part6 line 93
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20 line 95
  30. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode20 line 97
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode20Check line 99
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval20 line 101
  33. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode21 line 107
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode21 line 109
  35. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode21Check line 111
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval21 line 113
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode22 line 119
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode22 line 121
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode22Check line 123
  40. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval22 line 125
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode23 line 131
  42. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode23 line 133
  43. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode23Check line 135
  44. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval23 line 137
  45. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode24 line 143
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode24 line 145
  47. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode24Check line 147
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval24 line 149
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode25 line 155
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode25 line 157
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode25Check line 159
  52. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval25 line 161
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode26 line 167
  54. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode26 line 169
  55. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode26Check line 171
  56. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval26 line 173
  57. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode27 line 179
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode27 line 181
  59. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode27Check line 183
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval27 line 185
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode28 line 191
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode28 line 193
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode28Check line 195
  64. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval28 line 197
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode29 line 203
  66. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode29 line 205
  67. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode29Check line 207
  68. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval29 line 209
  69. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30part0 line 215
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30part1 line 217
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30part2 line 219
  72. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30part3 line 221
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30part4 line 223
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30part5 line 225
  75. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30 line 227
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode30 line 229
  77. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode30Check line 231
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval30 line 233
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode31 line 239
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode31 line 241
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode31Check line 243
  82. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval31 line 245