OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical1.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw16 line 16
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw16step0 line 18
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw16step1 line 20
  4. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw16step2 line 22
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw16step3 line 24
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw16step4 line 26
  7. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical16 line 28
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw17 line 62
  9. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw17step0 line 64
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw17step1 line 66
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical17 line 68
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw18 line 84
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw18step0 line 86
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw18step1 line 88
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw18step2 line 90
  16. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical18 line 92
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw19 line 113
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw19step0 line 115
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw19step1 line 117
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw19step2 line 119
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical19 line 121
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw20 line 143
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw20step0 line 145
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw20step1 line 147
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw20step2 line 149
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical20 line 151
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw21 line 172
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw21step0 line 174
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw21step1 line 176
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw21step2 line 178
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw21step3 line 180
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical21 line 182
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw22 line 211
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw22step0 line 213
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw22step1 line 215
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw22step2 line 217
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical22 line 219
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw23 line 240
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw23step0 line 242
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw23step1 line 244
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw23step2 line 246
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw23step3 line 248
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw23step4 line 250
  44. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical23 line 252
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw24 line 286
  46. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw24step0 line 288
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw24step1 line 290
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw24step2 line 292
  49. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical24 line 294
  50. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw25 line 316
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw25step0 line 318
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw25step1 line 320
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw25step2 line 322
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical25 line 324
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw26 line 345
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw26step0 line 347
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw26step1 line 349
  58. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical26 line 351
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw27 line 367
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw27step0 line 369
  61. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw27step1 line 371
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw27step2 line 373
  63. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical27 line 375
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw28 line 396
  65. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw28step0 line 398
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw28step1 line 400
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw28step2 line 402
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw28step3 line 404
  69. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical28 line 406
  70. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw29 line 435
  71. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw29step0 line 437
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw29step1 line 439
  73. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw29step2 line 441
  74. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical29 line 443
  75. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw30 line 464
  76. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw30step0 line 466
  77. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw30step1 line 468
  78. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw30step2 line 470
  79. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw30step3 line 472
  80. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw30step4 line 474
  81. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical30 line 476
  82. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw31 line 510
  83. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw31step0 line 512
  84. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw31step1 line 514
  85. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw31step2 line 516
  86. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical31 line 518