OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical243.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7776 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw7776step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw7776step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7776 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw7777 line 39
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical7777 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw7778 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw7778step0 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw7778step1 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7778 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw7779 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw7779step0 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw7779step1 line 68
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical7779 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw7780 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw7780step0 line 85
  17. def OAI.MUB6.Certificate.PairSemantics.raw7780step1 line 87
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical7780 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw7781 line 102
  20. def OAI.MUB6.Certificate.PairSemantics.raw7781step0 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw7781step1 line 106
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7781 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw7782 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw7782step0 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw7782step1 line 125
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7782 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw7783 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw7783step0 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw7783step1 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7783 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw7784 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw7784step0 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw7784step1 line 163
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7784 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw7785 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw7785step0 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw7785step1 line 182
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7785 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw7786 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw7786step0 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw7786step1 line 201
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7786 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw7787 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw7787step0 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw7787step1 line 220
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical7787 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw7788 line 235
  48. def OAI.MUB6.Certificate.PairSemantics.raw7788step0 line 237
  49. def OAI.MUB6.Certificate.PairSemantics.raw7788step1 line 239
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7788 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw7789 line 254
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7789 line 256
  53. def OAI.MUB6.Certificate.PairSemantics.raw7790 line 260
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7790 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw7791 line 266
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical7791 line 268
  57. def OAI.MUB6.Certificate.PairSemantics.raw7792 line 272
  58. def OAI.MUB6.Certificate.PairSemantics.raw7792step0 line 274
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7792 line 276
  60. def OAI.MUB6.Certificate.PairSemantics.raw7793 line 285
  61. def OAI.MUB6.Certificate.PairSemantics.raw7793step0 line 287
  62. def OAI.MUB6.Certificate.PairSemantics.raw7793step1 line 289
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical7793 line 291
  64. def OAI.MUB6.Certificate.PairSemantics.raw7794 line 304
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7794 line 306
  66. def OAI.MUB6.Certificate.PairSemantics.raw7795 line 310
  67. def OAI.MUB6.Certificate.PairSemantics.raw7795step0 line 312
  68. def OAI.MUB6.Certificate.PairSemantics.raw7795step1 line 314
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7795 line 316
  70. def OAI.MUB6.Certificate.PairSemantics.raw7796 line 329
  71. def OAI.MUB6.Certificate.PairSemantics.raw7796step0 line 331
  72. def OAI.MUB6.Certificate.PairSemantics.raw7796step1 line 333
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical7796 line 335
  74. def OAI.MUB6.Certificate.PairSemantics.raw7797 line 348
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7797 line 350
  76. def OAI.MUB6.Certificate.PairSemantics.raw7798 line 354
  77. def OAI.MUB6.Certificate.PairSemantics.raw7798step0 line 356
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7798 line 358
  79. def OAI.MUB6.Certificate.PairSemantics.raw7799 line 367
  80. def OAI.MUB6.Certificate.PairSemantics.raw7799step0 line 369
  81. def OAI.MUB6.Certificate.PairSemantics.raw7799step1 line 371
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7799 line 373
  83. def OAI.MUB6.Certificate.PairSemantics.raw7800 line 386
  84. def OAI.MUB6.Certificate.PairSemantics.raw7800step0 line 388
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7800 line 390
  86. def OAI.MUB6.Certificate.PairSemantics.raw7801 line 399
  87. def OAI.MUB6.Certificate.PairSemantics.raw7801step0 line 401
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical7801 line 403
  89. def OAI.MUB6.Certificate.PairSemantics.raw7802 line 412
  90. def OAI.MUB6.Certificate.PairSemantics.raw7802step0 line 414
  91. def OAI.MUB6.Certificate.PairSemantics.raw7802step1 line 416
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7802 line 418
  93. def OAI.MUB6.Certificate.PairSemantics.raw7803 line 431
  94. def OAI.MUB6.Certificate.PairSemantics.raw7803step0 line 433
  95. def OAI.MUB6.Certificate.PairSemantics.raw7803step1 line 435
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7803 line 437
  97. def OAI.MUB6.Certificate.PairSemantics.raw7804 line 450
  98. def OAI.MUB6.Certificate.PairSemantics.raw7804step0 line 452
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7804 line 454
  100. def OAI.MUB6.Certificate.PairSemantics.raw7805 line 463
  101. def OAI.MUB6.Certificate.PairSemantics.raw7805step0 line 465
  102. def OAI.MUB6.Certificate.PairSemantics.raw7805step1 line 467
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7805 line 469
  104. def OAI.MUB6.Certificate.PairSemantics.raw7806 line 482
  105. def OAI.MUB6.Certificate.PairSemantics.raw7806step0 line 484
  106. def OAI.MUB6.Certificate.PairSemantics.raw7806step1 line 486
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7806 line 488
  108. def OAI.MUB6.Certificate.PairSemantics.raw7807 line 501
  109. def OAI.MUB6.Certificate.PairSemantics.raw7807step0 line 503
  110. def OAI.MUB6.Certificate.PairSemantics.raw7807step1 line 505
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical7807 line 507