OAI/Analysis/MutuallyUnbiased/PairMoments/PairPermutations.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.pairPerm_0_1 line 8
  2. theorem OAI.MUB6.pairPerm_0_1_witness line 14
  3. def OAI.MUB6.pairPerm_0_2 line 23
  4. theorem OAI.MUB6.pairPerm_0_2_witness line 29
  5. def OAI.MUB6.pairPerm_0_3 line 38
  6. theorem OAI.MUB6.pairPerm_0_3_witness line 44
  7. def OAI.MUB6.pairPerm_0_4 line 53
  8. theorem OAI.MUB6.pairPerm_0_4_witness line 59
  9. def OAI.MUB6.pairPerm_0_5 line 68
  10. theorem OAI.MUB6.pairPerm_0_5_witness line 74
  11. def OAI.MUB6.pairPerm_1_0 line 83
  12. theorem OAI.MUB6.pairPerm_1_0_witness line 89
  13. def OAI.MUB6.pairPerm_1_2 line 98
  14. theorem OAI.MUB6.pairPerm_1_2_witness line 104
  15. def OAI.MUB6.pairPerm_1_3 line 113
  16. theorem OAI.MUB6.pairPerm_1_3_witness line 119
  17. def OAI.MUB6.pairPerm_1_4 line 128
  18. theorem OAI.MUB6.pairPerm_1_4_witness line 134
  19. def OAI.MUB6.pairPerm_1_5 line 143
  20. theorem OAI.MUB6.pairPerm_1_5_witness line 149
  21. def OAI.MUB6.pairPerm_2_0 line 158
  22. theorem OAI.MUB6.pairPerm_2_0_witness line 164
  23. def OAI.MUB6.pairPerm_2_1 line 173
  24. theorem OAI.MUB6.pairPerm_2_1_witness line 179
  25. def OAI.MUB6.pairPerm_2_3 line 188
  26. theorem OAI.MUB6.pairPerm_2_3_witness line 194
  27. def OAI.MUB6.pairPerm_2_4 line 203
  28. theorem OAI.MUB6.pairPerm_2_4_witness line 209
  29. def OAI.MUB6.pairPerm_2_5 line 218
  30. theorem OAI.MUB6.pairPerm_2_5_witness line 224
  31. def OAI.MUB6.pairPerm_3_0 line 233
  32. theorem OAI.MUB6.pairPerm_3_0_witness line 239
  33. def OAI.MUB6.pairPerm_3_1 line 248
  34. theorem OAI.MUB6.pairPerm_3_1_witness line 254
  35. def OAI.MUB6.pairPerm_3_2 line 263
  36. theorem OAI.MUB6.pairPerm_3_2_witness line 269
  37. def OAI.MUB6.pairPerm_3_4 line 278
  38. theorem OAI.MUB6.pairPerm_3_4_witness line 284
  39. def OAI.MUB6.pairPerm_3_5 line 293
  40. theorem OAI.MUB6.pairPerm_3_5_witness line 299
  41. def OAI.MUB6.pairPerm_4_0 line 308
  42. theorem OAI.MUB6.pairPerm_4_0_witness line 314
  43. def OAI.MUB6.pairPerm_4_1 line 323
  44. theorem OAI.MUB6.pairPerm_4_1_witness line 329
  45. def OAI.MUB6.pairPerm_4_2 line 338
  46. theorem OAI.MUB6.pairPerm_4_2_witness line 344
  47. def OAI.MUB6.pairPerm_4_3 line 353
  48. theorem OAI.MUB6.pairPerm_4_3_witness line 359
  49. def OAI.MUB6.pairPerm_4_5 line 368
  50. theorem OAI.MUB6.pairPerm_4_5_witness line 374
  51. def OAI.MUB6.pairPerm_5_0 line 383
  52. theorem OAI.MUB6.pairPerm_5_0_witness line 389
  53. def OAI.MUB6.pairPerm_5_1 line 398
  54. theorem OAI.MUB6.pairPerm_5_1_witness line 404
  55. def OAI.MUB6.pairPerm_5_2 line 413
  56. theorem OAI.MUB6.pairPerm_5_2_witness line 419
  57. def OAI.MUB6.pairPerm_5_3 line 428
  58. theorem OAI.MUB6.pairPerm_5_3_witness line 434
  59. def OAI.MUB6.pairPerm_5_4 line 443
  60. theorem OAI.MUB6.pairPerm_5_4_witness line 449
  61. theorem OAI.MUB6.pair_permutation_witness line 458