OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical300.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9600 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw9600step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9600 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw9601 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw9601step0 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9601 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw9602 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw9602step0 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw9602step1 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9602 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw9603 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw9603step0 line 63
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9603 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw9604 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw9604step0 line 76
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical9604 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw9605 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw9605step0 line 89
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9605 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw9606 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw9606step0 line 102
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9606 line 104
  23. def OAI.MUB6.Certificate.PairSemantics.raw9607 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw9607step0 line 115
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9607 line 117
  26. def OAI.MUB6.Certificate.PairSemantics.raw9608 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw9608step0 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw9608step1 line 130
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9608 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw9609 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw9609step0 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw9609step1 line 149
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9609 line 151
  34. def OAI.MUB6.Certificate.PairSemantics.raw9610 line 164
  35. def OAI.MUB6.Certificate.PairSemantics.raw9610step0 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw9610step1 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9610 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw9611 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw9611step0 line 185
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9611 line 187
  41. def OAI.MUB6.Certificate.PairSemantics.raw9612 line 196
  42. def OAI.MUB6.Certificate.PairSemantics.raw9612step0 line 198
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9612 line 200
  44. def OAI.MUB6.Certificate.PairSemantics.raw9613 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw9613step0 line 211
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9613 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw9614 line 222
  48. def OAI.MUB6.Certificate.PairSemantics.raw9614step0 line 224
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical9614 line 226
  50. def OAI.MUB6.Certificate.PairSemantics.raw9615 line 235
  51. def OAI.MUB6.Certificate.PairSemantics.raw9615step0 line 237
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9615 line 239
  53. def OAI.MUB6.Certificate.PairSemantics.raw9616 line 248
  54. def OAI.MUB6.Certificate.PairSemantics.raw9616step0 line 250
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9616 line 252
  56. def OAI.MUB6.Certificate.PairSemantics.raw9617 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw9617step0 line 263
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9617 line 265
  59. def OAI.MUB6.Certificate.PairSemantics.raw9618 line 274
  60. def OAI.MUB6.Certificate.PairSemantics.raw9618step0 line 276
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9618 line 278
  62. def OAI.MUB6.Certificate.PairSemantics.raw9619 line 287
  63. def OAI.MUB6.Certificate.PairSemantics.raw9619step0 line 289
  64. def OAI.MUB6.Certificate.PairSemantics.raw9619step1 line 291
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9619 line 293
  66. def OAI.MUB6.Certificate.PairSemantics.raw9620 line 306
  67. def OAI.MUB6.Certificate.PairSemantics.raw9620step0 line 308
  68. def OAI.MUB6.Certificate.PairSemantics.raw9620step1 line 310
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9620 line 312
  70. def OAI.MUB6.Certificate.PairSemantics.raw9621 line 325
  71. def OAI.MUB6.Certificate.PairSemantics.raw9621step0 line 327
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9621 line 329
  73. def OAI.MUB6.Certificate.PairSemantics.raw9622 line 338
  74. def OAI.MUB6.Certificate.PairSemantics.raw9622step0 line 340
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9622 line 342
  76. def OAI.MUB6.Certificate.PairSemantics.raw9623 line 351
  77. def OAI.MUB6.Certificate.PairSemantics.raw9623step0 line 353
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9623 line 355
  79. def OAI.MUB6.Certificate.PairSemantics.raw9624 line 364
  80. def OAI.MUB6.Certificate.PairSemantics.raw9624step0 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw9624step1 line 368
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9624 line 370
  83. def OAI.MUB6.Certificate.PairSemantics.raw9625 line 383
  84. def OAI.MUB6.Certificate.PairSemantics.raw9625step0 line 385
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9625 line 387
  86. def OAI.MUB6.Certificate.PairSemantics.raw9626 line 396
  87. def OAI.MUB6.Certificate.PairSemantics.raw9626step0 line 398
  88. def OAI.MUB6.Certificate.PairSemantics.raw9626step1 line 400
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9626 line 402
  90. def OAI.MUB6.Certificate.PairSemantics.raw9627 line 415
  91. def OAI.MUB6.Certificate.PairSemantics.raw9627step0 line 417
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9627 line 419
  93. def OAI.MUB6.Certificate.PairSemantics.raw9628 line 428
  94. def OAI.MUB6.Certificate.PairSemantics.raw9628step0 line 430
  95. def OAI.MUB6.Certificate.PairSemantics.raw9628step1 line 432
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9628 line 434
  97. def OAI.MUB6.Certificate.PairSemantics.raw9629 line 447
  98. def OAI.MUB6.Certificate.PairSemantics.raw9629step0 line 449
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9629 line 451
  100. def OAI.MUB6.Certificate.PairSemantics.raw9630 line 460
  101. def OAI.MUB6.Certificate.PairSemantics.raw9630step0 line 462
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9630 line 464
  103. def OAI.MUB6.Certificate.PairSemantics.raw9631 line 473
  104. def OAI.MUB6.Certificate.PairSemantics.raw9631step0 line 475
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical9631 line 477