OAI/Analysis/MutuallyUnbiased/MixedTargets/OriginalMerge3.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode48 line 25
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode48 line 27
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode48Check line 29
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval48 line 31
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode49 line 37
  6. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode49 line 39
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode49Check line 41
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval49 line 43
  9. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode50 line 49
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode50 line 51
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode50Check line 53
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval50 line 55
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode51 line 61
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode51 line 63
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode51Check line 65
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval51 line 67
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode52 line 73
  18. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode52 line 75
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode52Check line 77
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval52 line 79
  21. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53part0 line 85
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53part1 line 87
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53part2 line 89
  24. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53part3 line 91
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53part4 line 93
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53part5 line 95
  27. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53 line 97
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode53 line 99
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode53Check line 101
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval53 line 103
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode54 line 109
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode54 line 111
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode54Check line 113
  34. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval54 line 115
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode55 line 121
  36. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode55 line 123
  37. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode55Check line 125
  38. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval55 line 127
  39. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode56 line 133
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode56 line 135
  41. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode56Check line 137
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval56 line 139
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode57 line 145
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode57 line 147
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode57Check line 149
  46. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval57 line 151
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode58 line 157
  48. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode58 line 159
  49. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode58Check line 161
  50. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval58 line 163
  51. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode59 line 169
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode59 line 171
  53. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode59Check line 173
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval59 line 175
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode60 line 181
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode60 line 183
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode60Check line 185
  58. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval60 line 187
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode61 line 193
  60. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode61 line 195
  61. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode61Check line 197
  62. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval61 line 199
  63. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode62 line 205
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode62 line 207
  65. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode62Check line 209
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval62 line 211
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode63 line 217
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode63 line 219
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode63Check line 221
  70. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval63 line 223