OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical275.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8800 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw8800step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw8800step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8800 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw8801 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw8801step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw8801step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8801 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw8802 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw8802step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw8802step1 line 64
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8802 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw8803 line 79
  14. def OAI.MUB6.Certificate.PairSemantics.raw8803step0 line 81
  15. def OAI.MUB6.Certificate.PairSemantics.raw8803step1 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw8803step2 line 85
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8803 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw8804 line 104
  19. def OAI.MUB6.Certificate.PairSemantics.raw8804step0 line 106
  20. def OAI.MUB6.Certificate.PairSemantics.raw8804step1 line 108
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8804 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw8805 line 123
  23. def OAI.MUB6.Certificate.PairSemantics.raw8805step0 line 125
  24. def OAI.MUB6.Certificate.PairSemantics.raw8805step1 line 127
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8805 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw8806 line 142
  27. def OAI.MUB6.Certificate.PairSemantics.raw8806step0 line 144
  28. def OAI.MUB6.Certificate.PairSemantics.raw8806step1 line 146
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8806 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw8807 line 161
  31. def OAI.MUB6.Certificate.PairSemantics.raw8807step0 line 163
  32. def OAI.MUB6.Certificate.PairSemantics.raw8807step1 line 165
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8807 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw8808 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw8808step0 line 182
  36. def OAI.MUB6.Certificate.PairSemantics.raw8808step1 line 184
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8808 line 186
  38. def OAI.MUB6.Certificate.PairSemantics.raw8809 line 199
  39. def OAI.MUB6.Certificate.PairSemantics.raw8809step0 line 201
  40. def OAI.MUB6.Certificate.PairSemantics.raw8809step1 line 203
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical8809 line 205
  42. def OAI.MUB6.Certificate.PairSemantics.raw8810 line 218
  43. def OAI.MUB6.Certificate.PairSemantics.raw8810step0 line 220
  44. def OAI.MUB6.Certificate.PairSemantics.raw8810step1 line 222
  45. def OAI.MUB6.Certificate.PairSemantics.raw8810step2 line 224
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical8810 line 226
  47. def OAI.MUB6.Certificate.PairSemantics.raw8811 line 243
  48. def OAI.MUB6.Certificate.PairSemantics.raw8811step0 line 245
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8811 line 247
  50. def OAI.MUB6.Certificate.PairSemantics.raw8812 line 256
  51. def OAI.MUB6.Certificate.PairSemantics.raw8812step0 line 258
  52. def OAI.MUB6.Certificate.PairSemantics.raw8812step1 line 260
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8812 line 262
  54. def OAI.MUB6.Certificate.PairSemantics.raw8813 line 275
  55. def OAI.MUB6.Certificate.PairSemantics.raw8813step0 line 277
  56. def OAI.MUB6.Certificate.PairSemantics.raw8813step1 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw8813step2 line 281
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8813 line 283
  59. def OAI.MUB6.Certificate.PairSemantics.raw8814 line 300
  60. def OAI.MUB6.Certificate.PairSemantics.raw8814step0 line 302
  61. def OAI.MUB6.Certificate.PairSemantics.raw8814step1 line 304
  62. def OAI.MUB6.Certificate.PairSemantics.raw8814step2 line 306
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical8814 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw8815 line 325
  65. def OAI.MUB6.Certificate.PairSemantics.raw8815step0 line 327
  66. def OAI.MUB6.Certificate.PairSemantics.raw8815step1 line 329
  67. def OAI.MUB6.Certificate.PairSemantics.raw8815step2 line 331
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8815 line 333
  69. def OAI.MUB6.Certificate.PairSemantics.raw8816 line 350
  70. def OAI.MUB6.Certificate.PairSemantics.raw8816step0 line 352
  71. def OAI.MUB6.Certificate.PairSemantics.raw8816step1 line 354
  72. def OAI.MUB6.Certificate.PairSemantics.raw8816step2 line 356
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8816 line 358
  74. def OAI.MUB6.Certificate.PairSemantics.raw8817 line 375
  75. def OAI.MUB6.Certificate.PairSemantics.raw8817step0 line 377
  76. def OAI.MUB6.Certificate.PairSemantics.raw8817step1 line 379
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8817 line 381
  78. def OAI.MUB6.Certificate.PairSemantics.raw8818 line 394
  79. def OAI.MUB6.Certificate.PairSemantics.raw8818step0 line 396
  80. def OAI.MUB6.Certificate.PairSemantics.raw8818step1 line 398
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8818 line 400
  82. def OAI.MUB6.Certificate.PairSemantics.raw8819 line 413
  83. def OAI.MUB6.Certificate.PairSemantics.raw8819step0 line 415
  84. def OAI.MUB6.Certificate.PairSemantics.raw8819step1 line 417
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8819 line 419
  86. def OAI.MUB6.Certificate.PairSemantics.raw8820 line 433
  87. def OAI.MUB6.Certificate.PairSemantics.raw8820step0 line 435
  88. def OAI.MUB6.Certificate.PairSemantics.raw8820step1 line 437
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8820 line 439
  90. def OAI.MUB6.Certificate.PairSemantics.raw8821 line 452
  91. def OAI.MUB6.Certificate.PairSemantics.raw8821step0 line 454
  92. def OAI.MUB6.Certificate.PairSemantics.raw8821step1 line 456
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8821 line 458
  94. def OAI.MUB6.Certificate.PairSemantics.raw8822 line 471
  95. def OAI.MUB6.Certificate.PairSemantics.raw8822step0 line 473
  96. def OAI.MUB6.Certificate.PairSemantics.raw8822step1 line 475
  97. def OAI.MUB6.Certificate.PairSemantics.raw8822step2 line 477
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical8822 line 479
  99. def OAI.MUB6.Certificate.PairSemantics.raw8823 line 497
  100. def OAI.MUB6.Certificate.PairSemantics.raw8823step0 line 499
  101. def OAI.MUB6.Certificate.PairSemantics.raw8823step1 line 501
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8823 line 503
  103. def OAI.MUB6.Certificate.PairSemantics.raw8824 line 516
  104. def OAI.MUB6.Certificate.PairSemantics.raw8824step0 line 518
  105. def OAI.MUB6.Certificate.PairSemantics.raw8824step1 line 520
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8824 line 522
  107. def OAI.MUB6.Certificate.PairSemantics.raw8825 line 535
  108. def OAI.MUB6.Certificate.PairSemantics.raw8825step0 line 537
  109. def OAI.MUB6.Certificate.PairSemantics.raw8825step1 line 539
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8825 line 541
  111. def OAI.MUB6.Certificate.PairSemantics.raw8826 line 554
  112. def OAI.MUB6.Certificate.PairSemantics.raw8826step0 line 556
  113. def OAI.MUB6.Certificate.PairSemantics.raw8826step1 line 558
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8826 line 560
  115. def OAI.MUB6.Certificate.PairSemantics.raw8827 line 573
  116. def OAI.MUB6.Certificate.PairSemantics.raw8827step0 line 575
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical8827 line 577
  118. def OAI.MUB6.Certificate.PairSemantics.raw8828 line 586
  119. def OAI.MUB6.Certificate.PairSemantics.raw8828step0 line 588
  120. def OAI.MUB6.Certificate.PairSemantics.raw8828step1 line 590
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical8828 line 592
  122. def OAI.MUB6.Certificate.PairSemantics.raw8829 line 605
  123. def OAI.MUB6.Certificate.PairSemantics.raw8829step0 line 607
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical8829 line 609
  125. def OAI.MUB6.Certificate.PairSemantics.raw8830 line 618
  126. def OAI.MUB6.Certificate.PairSemantics.raw8830step0 line 620
  127. def OAI.MUB6.Certificate.PairSemantics.raw8830step1 line 622
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical8830 line 624
  129. def OAI.MUB6.Certificate.PairSemantics.raw8831 line 637
  130. def OAI.MUB6.Certificate.PairSemantics.raw8831step0 line 639
  131. def OAI.MUB6.Certificate.PairSemantics.raw8831step1 line 641
  132. def OAI.MUB6.Certificate.PairSemantics.raw8831step2 line 643
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical8831 line 645