OAI/Analysis/MutuallyUnbiased/MixedTargets/OriginalMerge0.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode0 line 25
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode0 line 27
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode0Check line 29
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval0 line 31
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode1 line 37
  6. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode1 line 39
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode1Check line 41
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval1 line 43
  9. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode2 line 49
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode2 line 51
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode2Check line 53
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval2 line 55
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode3 line 61
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode3 line 63
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode3Check line 65
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval3 line 67
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode4 line 73
  18. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode4 line 75
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode4Check line 77
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval4 line 79
  21. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode5 line 85
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode5 line 87
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode5Check line 89
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval5 line 91
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode6 line 97
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode6 line 99
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode6Check line 101
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval6 line 103
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode7 line 109
  30. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode7 line 111
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode7Check line 113
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval7 line 115
  33. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode8 line 121
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode8 line 123
  35. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode8Check line 125
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval8 line 127
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode9 line 133
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode9 line 135
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode9Check line 137
  40. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval9 line 139
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode10 line 145
  42. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode10 line 147
  43. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode10Check line 149
  44. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval10 line 151
  45. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode11 line 157
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode11 line 159
  47. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode11Check line 161
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval11 line 163
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode12 line 169
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode12 line 171
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode12Check line 173
  52. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval12 line 175
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode13 line 181
  54. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode13 line 183
  55. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode13Check line 185
  56. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval13 line 187
  57. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode14 line 193
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode14 line 195
  59. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode14Check line 197
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval14 line 199
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode15 line 205
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode15 line 207
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode15Check line 209
  64. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval15 line 211