OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical253.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8096 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw8096step0 line 25
  3. def OAI.MUB6.Certificate.PairSemantics.raw8096step1 line 27
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8096 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw8097 line 43
  6. def OAI.MUB6.Certificate.PairSemantics.raw8097step0 line 45
  7. def OAI.MUB6.Certificate.PairSemantics.raw8097step1 line 47
  8. def OAI.MUB6.Certificate.PairSemantics.raw8097step2 line 49
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8097 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw8098 line 69
  11. def OAI.MUB6.Certificate.PairSemantics.raw8098step0 line 71
  12. def OAI.MUB6.Certificate.PairSemantics.raw8098step1 line 73
  13. def OAI.MUB6.Certificate.PairSemantics.raw8098step2 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw8098step3 line 77
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8098 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw8099 line 101
  17. def OAI.MUB6.Certificate.PairSemantics.raw8099step0 line 103
  18. def OAI.MUB6.Certificate.PairSemantics.raw8099step1 line 105
  19. def OAI.MUB6.Certificate.PairSemantics.raw8099step2 line 107
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8099 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw8100 line 127
  22. def OAI.MUB6.Certificate.PairSemantics.raw8100step0 line 129
  23. def OAI.MUB6.Certificate.PairSemantics.raw8100step1 line 131
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8100 line 133
  25. def OAI.MUB6.Certificate.PairSemantics.raw8101 line 146
  26. def OAI.MUB6.Certificate.PairSemantics.raw8101step0 line 148
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8101 line 150
  28. def OAI.MUB6.Certificate.PairSemantics.raw8102 line 159
  29. def OAI.MUB6.Certificate.PairSemantics.raw8102step0 line 161
  30. def OAI.MUB6.Certificate.PairSemantics.raw8102step1 line 163
  31. def OAI.MUB6.Certificate.PairSemantics.raw8102step2 line 165
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8102 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw8103 line 185
  34. def OAI.MUB6.Certificate.PairSemantics.raw8103step0 line 187
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8103 line 189
  36. def OAI.MUB6.Certificate.PairSemantics.raw8104 line 198
  37. def OAI.MUB6.Certificate.PairSemantics.raw8104step0 line 200
  38. def OAI.MUB6.Certificate.PairSemantics.raw8104step1 line 202
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8104 line 204
  40. def OAI.MUB6.Certificate.PairSemantics.raw8105 line 217
  41. def OAI.MUB6.Certificate.PairSemantics.raw8105step0 line 219
  42. def OAI.MUB6.Certificate.PairSemantics.raw8105step1 line 221
  43. def OAI.MUB6.Certificate.PairSemantics.raw8105step2 line 223
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8105 line 225
  45. def OAI.MUB6.Certificate.PairSemantics.raw8106 line 243
  46. def OAI.MUB6.Certificate.PairSemantics.raw8106step0 line 245
  47. def OAI.MUB6.Certificate.PairSemantics.raw8106step1 line 247
  48. def OAI.MUB6.Certificate.PairSemantics.raw8106step2 line 249
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8106 line 251
  50. def OAI.MUB6.Certificate.PairSemantics.raw8107 line 269
  51. def OAI.MUB6.Certificate.PairSemantics.raw8107step0 line 271
  52. def OAI.MUB6.Certificate.PairSemantics.raw8107step1 line 273
  53. def OAI.MUB6.Certificate.PairSemantics.raw8107step2 line 275
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8107 line 277
  55. def OAI.MUB6.Certificate.PairSemantics.raw8108 line 295
  56. def OAI.MUB6.Certificate.PairSemantics.raw8108step0 line 297
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8108 line 299
  58. def OAI.MUB6.Certificate.PairSemantics.raw8109 line 308
  59. def OAI.MUB6.Certificate.PairSemantics.raw8109step0 line 310
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8109 line 312
  61. def OAI.MUB6.Certificate.PairSemantics.raw8110 line 321
  62. def OAI.MUB6.Certificate.PairSemantics.raw8110step0 line 323
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical8110 line 325
  64. def OAI.MUB6.Certificate.PairSemantics.raw8111 line 334
  65. def OAI.MUB6.Certificate.PairSemantics.raw8111step0 line 336
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8111 line 338
  67. def OAI.MUB6.Certificate.PairSemantics.raw8112 line 347
  68. def OAI.MUB6.Certificate.PairSemantics.raw8112step0 line 349
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8112 line 351
  70. def OAI.MUB6.Certificate.PairSemantics.raw8113 line 360
  71. def OAI.MUB6.Certificate.PairSemantics.raw8113step0 line 362
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8113 line 364
  73. def OAI.MUB6.Certificate.PairSemantics.raw8114 line 373
  74. def OAI.MUB6.Certificate.PairSemantics.raw8114step0 line 375
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8114 line 377
  76. def OAI.MUB6.Certificate.PairSemantics.raw8115 line 386
  77. def OAI.MUB6.Certificate.PairSemantics.raw8115step0 line 388
  78. def OAI.MUB6.Certificate.PairSemantics.raw8115step1 line 390
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8115 line 392
  80. def OAI.MUB6.Certificate.PairSemantics.raw8116 line 405
  81. def OAI.MUB6.Certificate.PairSemantics.raw8116step0 line 407
  82. def OAI.MUB6.Certificate.PairSemantics.raw8116step1 line 409
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8116 line 411
  84. def OAI.MUB6.Certificate.PairSemantics.raw8117 line 424
  85. def OAI.MUB6.Certificate.PairSemantics.raw8117step0 line 426
  86. def OAI.MUB6.Certificate.PairSemantics.raw8117step1 line 428
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8117 line 430
  88. def OAI.MUB6.Certificate.PairSemantics.raw8118 line 443
  89. def OAI.MUB6.Certificate.PairSemantics.raw8118step0 line 445
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical8118 line 447
  91. def OAI.MUB6.Certificate.PairSemantics.raw8119 line 456
  92. def OAI.MUB6.Certificate.PairSemantics.raw8119step0 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw8119step1 line 460
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8119 line 462
  95. def OAI.MUB6.Certificate.PairSemantics.raw8120 line 475
  96. def OAI.MUB6.Certificate.PairSemantics.raw8120step0 line 477
  97. def OAI.MUB6.Certificate.PairSemantics.raw8120step1 line 479
  98. def OAI.MUB6.Certificate.PairSemantics.raw8120step2 line 481
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8120 line 483
  100. def OAI.MUB6.Certificate.PairSemantics.raw8121 line 501
  101. def OAI.MUB6.Certificate.PairSemantics.raw8121step0 line 503
  102. def OAI.MUB6.Certificate.PairSemantics.raw8121step1 line 505
  103. def OAI.MUB6.Certificate.PairSemantics.raw8121step2 line 507
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8121 line 509
  105. def OAI.MUB6.Certificate.PairSemantics.raw8122 line 527
  106. def OAI.MUB6.Certificate.PairSemantics.raw8122step0 line 529
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8122 line 531
  108. def OAI.MUB6.Certificate.PairSemantics.raw8123 line 540
  109. def OAI.MUB6.Certificate.PairSemantics.raw8123step0 line 542
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8123 line 544
  111. def OAI.MUB6.Certificate.PairSemantics.raw8124 line 553
  112. def OAI.MUB6.Certificate.PairSemantics.raw8124step0 line 555
  113. def OAI.MUB6.Certificate.PairSemantics.raw8124step1 line 557
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8124 line 559
  115. def OAI.MUB6.Certificate.PairSemantics.raw8125 line 572
  116. def OAI.MUB6.Certificate.PairSemantics.raw8125step0 line 574
  117. def OAI.MUB6.Certificate.PairSemantics.raw8125step1 line 576
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical8125 line 578
  119. def OAI.MUB6.Certificate.PairSemantics.raw8126 line 591
  120. def OAI.MUB6.Certificate.PairSemantics.raw8126step0 line 593
  121. def OAI.MUB6.Certificate.PairSemantics.raw8126step1 line 595
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical8126 line 597
  123. def OAI.MUB6.Certificate.PairSemantics.raw8127 line 610
  124. def OAI.MUB6.Certificate.PairSemantics.raw8127step0 line 612
  125. def OAI.MUB6.Certificate.PairSemantics.raw8127step1 line 614
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical8127 line 616