OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraPermutations.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation0 line 7
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation1 line 13
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation2 line 19
  4. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation3 line 25
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation4 line 31
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation5 line 37
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation6 line 43
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation7 line 49
  9. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation8 line 55
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation9 line 61
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation10 line 67
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation11 line 73
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation12 line 79
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation13 line 85
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation14 line 91
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation15 line 97
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation16 line 103
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation17 line 109
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation18 line 115
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation19 line 121
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation20 line 127
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation21 line 133
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation22 line 139
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation23 line 145
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation24 line 151
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation25 line 157
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation26 line 163
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation27 line 169
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation28 line 175
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation29 line 181
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation30 line 187
  32. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation31 line 193
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation32 line 199
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation33 line 205
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation34 line 211
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation35 line 217
  37. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation36 line 223
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation37 line 229
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation38 line 235
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation39 line 241
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation40 line 247
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation41 line 253
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation42 line 259
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation43 line 265
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation44 line 271
  46. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation45 line 277
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation46 line 283
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation47 line 289
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation48 line 295
  50. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation49 line 301
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation50 line 307
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation51 line 313
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation52 line 319
  54. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation53 line 325
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation54 line 331
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation55 line 337
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation56 line 343
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation57 line 349
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation58 line 355
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation59 line 361
  61. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation60 line 367
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation61 line 373
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation62 line 379
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation63 line 385
  65. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation64 line 391
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation65 line 397
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation66 line 403
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraPermutation67 line 409