OAI/Analysis/MutuallyUnbiased/MixedTargets/OriginalMerge4.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64part0 line 24
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64part1 line 26
  3. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64part2 line 28
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64part3 line 30
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64part4 line 32
  6. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64part5 line 34
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64 line 36
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode64 line 38
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode64Check line 40
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval64 line 42
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part0 line 48
  12. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part1 line 50
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part2 line 52
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part3 line 54
  15. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part4 line 56
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part5 line 58
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part6 line 60
  18. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part7 line 62
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part8 line 64
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65part9 line 66
  21. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65 line 68
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode65 line 70
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode65Check line 72
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval65 line 74
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode66 line 80
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode66 line 82
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode66Check line 84
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval66 line 86
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode67 line 92
  30. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode67 line 94
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode67Check line 96
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval67 line 98
  33. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode68 line 104
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode68 line 106
  35. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode68Check line 108
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval68 line 110
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69part0 line 116
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69part1 line 118
  39. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69part2 line 120
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69part3 line 122
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69part4 line 124
  42. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69 line 126
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode69 line 128
  44. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode69Check line 130
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval69 line 132
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode70 line 138
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode70 line 140
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode70Check line 142
  49. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval70 line 144
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode71 line 150
  51. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode71 line 152
  52. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode71Check line 154
  53. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval71 line 156
  54. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode72 line 162
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode72 line 164
  56. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode72Check line 166
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval72 line 168
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode73 line 174
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode73 line 176
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode73Check line 178
  61. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval73 line 180
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74part0 line 186
  63. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74part1 line 188
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74part2 line 190
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74part3 line 192
  66. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74part4 line 194
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74 line 196
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode74 line 198
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode74Check line 200
  70. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval74 line 202
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part0 line 208
  72. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part1 line 210
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part2 line 212
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part3 line 214
  75. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part4 line 216
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part5 line 218
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part6 line 220
  78. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part7 line 222
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75part8 line 224
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75 line 226
  81. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode75 line 228
  82. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode75Check line 230
  83. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval75 line 232
  84. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode76 line 238
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode76 line 240
  86. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode76Check line 242
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval76 line 244
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode77 line 250
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode77 line 252
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode77Check line 254
  91. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval77 line 256
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode78 line 262
  93. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode78 line 264
  94. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode78Check line 266
  95. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval78 line 268
  96. def OAI.MUB6.Certificate.MixedTargetSemantics.originalNode79 line 274
  97. def OAI.MUB6.Certificate.MixedTargetSemantics.keyPolynomialNode79 line 276
  98. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNode79Check line 278
  99. theorem OAI.MUB6.Certificate.MixedTargetSemantics.originalNodeEval79 line 280