OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical306.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9792 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw9792step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9792 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw9793 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw9793step0 line 33
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9793 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw9794 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw9794step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9794 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw9795 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw9795step0 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9795 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw9796 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw9796step0 line 72
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9796 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw9797 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw9797step0 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw9797step1 line 87
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9797 line 89
  20. def OAI.MUB6.Certificate.PairSemantics.raw9798 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw9798step0 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9798 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw9799 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw9799step0 line 118
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9799 line 120
  26. def OAI.MUB6.Certificate.PairSemantics.raw9800 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw9800step0 line 131
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9800 line 133
  29. def OAI.MUB6.Certificate.PairSemantics.raw9801 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw9801step0 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9801 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw9802 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw9802step0 line 157
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9802 line 159
  35. def OAI.MUB6.Certificate.PairSemantics.raw9803 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw9803step0 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw9803step1 line 172
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9803 line 174
  39. def OAI.MUB6.Certificate.PairSemantics.raw9804 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw9804step0 line 190
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9804 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw9805 line 201
  43. def OAI.MUB6.Certificate.PairSemantics.raw9805step0 line 203
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9805 line 205
  45. def OAI.MUB6.Certificate.PairSemantics.raw9806 line 214
  46. def OAI.MUB6.Certificate.PairSemantics.raw9806step0 line 216
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9806 line 218
  48. def OAI.MUB6.Certificate.PairSemantics.raw9807 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw9807step0 line 229
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9807 line 231
  51. def OAI.MUB6.Certificate.PairSemantics.raw9808 line 240
  52. def OAI.MUB6.Certificate.PairSemantics.raw9808step0 line 242
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9808 line 244
  54. def OAI.MUB6.Certificate.PairSemantics.raw9809 line 253
  55. def OAI.MUB6.Certificate.PairSemantics.raw9809step0 line 255
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9809 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw9810 line 266
  58. def OAI.MUB6.Certificate.PairSemantics.raw9810step0 line 268
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9810 line 270
  60. def OAI.MUB6.Certificate.PairSemantics.raw9811 line 279
  61. def OAI.MUB6.Certificate.PairSemantics.raw9811step0 line 281
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9811 line 283
  63. def OAI.MUB6.Certificate.PairSemantics.raw9812 line 292
  64. def OAI.MUB6.Certificate.PairSemantics.raw9812step0 line 294
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9812 line 296
  66. def OAI.MUB6.Certificate.PairSemantics.raw9813 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw9813step0 line 307
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9813 line 309
  69. def OAI.MUB6.Certificate.PairSemantics.raw9814 line 318
  70. def OAI.MUB6.Certificate.PairSemantics.raw9814step0 line 320
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9814 line 322
  72. def OAI.MUB6.Certificate.PairSemantics.raw9815 line 331
  73. def OAI.MUB6.Certificate.PairSemantics.raw9815step0 line 333
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9815 line 335
  75. def OAI.MUB6.Certificate.PairSemantics.raw9816 line 344
  76. def OAI.MUB6.Certificate.PairSemantics.raw9816step0 line 346
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9816 line 348
  78. def OAI.MUB6.Certificate.PairSemantics.raw9817 line 357
  79. def OAI.MUB6.Certificate.PairSemantics.raw9817step0 line 359
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical9817 line 361
  81. def OAI.MUB6.Certificate.PairSemantics.raw9818 line 370
  82. def OAI.MUB6.Certificate.PairSemantics.raw9818step0 line 372
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9818 line 374
  84. def OAI.MUB6.Certificate.PairSemantics.raw9819 line 383
  85. def OAI.MUB6.Certificate.PairSemantics.raw9819step0 line 385
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9819 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw9820 line 396
  88. def OAI.MUB6.Certificate.PairSemantics.raw9820step0 line 398
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9820 line 400
  90. def OAI.MUB6.Certificate.PairSemantics.raw9821 line 409
  91. def OAI.MUB6.Certificate.PairSemantics.raw9821step0 line 411
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9821 line 413
  93. def OAI.MUB6.Certificate.PairSemantics.raw9822 line 422
  94. def OAI.MUB6.Certificate.PairSemantics.raw9822step0 line 424
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9822 line 426
  96. def OAI.MUB6.Certificate.PairSemantics.raw9823 line 435
  97. def OAI.MUB6.Certificate.PairSemantics.raw9823step0 line 437
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9823 line 439