OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical271.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8672 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8672step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8672 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8673 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw8673step0 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw8673step1 line 36
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8673 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw8674 line 51
  9. def OAI.MUB6.Certificate.PairSemantics.raw8674step0 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw8674step1 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical8674 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw8675 line 71
  13. def OAI.MUB6.Certificate.PairSemantics.raw8675step0 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw8675step1 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw8675step2 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8675 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw8676 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw8676step0 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw8676step1 line 101
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8676 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw8677 line 117
  22. def OAI.MUB6.Certificate.PairSemantics.raw8677step0 line 119
  23. def OAI.MUB6.Certificate.PairSemantics.raw8677step1 line 121
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8677 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw8678 line 137
  26. def OAI.MUB6.Certificate.PairSemantics.raw8678step0 line 139
  27. def OAI.MUB6.Certificate.PairSemantics.raw8678step1 line 141
  28. def OAI.MUB6.Certificate.PairSemantics.raw8678step2 line 143
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8678 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw8679 line 163
  31. def OAI.MUB6.Certificate.PairSemantics.raw8679step0 line 165
  32. def OAI.MUB6.Certificate.PairSemantics.raw8679step1 line 167
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8679 line 169
  34. def OAI.MUB6.Certificate.PairSemantics.raw8680 line 183
  35. def OAI.MUB6.Certificate.PairSemantics.raw8680step0 line 185
  36. def OAI.MUB6.Certificate.PairSemantics.raw8680step1 line 187
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8680 line 189
  38. def OAI.MUB6.Certificate.PairSemantics.raw8681 line 203
  39. def OAI.MUB6.Certificate.PairSemantics.raw8681step0 line 205
  40. def OAI.MUB6.Certificate.PairSemantics.raw8681step1 line 207
  41. def OAI.MUB6.Certificate.PairSemantics.raw8681step2 line 209
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8681 line 211
  43. def OAI.MUB6.Certificate.PairSemantics.raw8682 line 229
  44. def OAI.MUB6.Certificate.PairSemantics.raw8682step0 line 231
  45. def OAI.MUB6.Certificate.PairSemantics.raw8682step1 line 233
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical8682 line 235
  47. def OAI.MUB6.Certificate.PairSemantics.raw8683 line 249
  48. def OAI.MUB6.Certificate.PairSemantics.raw8683step0 line 251
  49. def OAI.MUB6.Certificate.PairSemantics.raw8683step1 line 253
  50. def OAI.MUB6.Certificate.PairSemantics.raw8683step2 line 255
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8683 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw8684 line 275
  53. def OAI.MUB6.Certificate.PairSemantics.raw8684step0 line 277
  54. def OAI.MUB6.Certificate.PairSemantics.raw8684step1 line 279
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8684 line 281
  56. def OAI.MUB6.Certificate.PairSemantics.raw8685 line 295
  57. def OAI.MUB6.Certificate.PairSemantics.raw8685step0 line 297
  58. def OAI.MUB6.Certificate.PairSemantics.raw8685step1 line 299
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8685 line 301
  60. def OAI.MUB6.Certificate.PairSemantics.raw8686 line 315
  61. def OAI.MUB6.Certificate.PairSemantics.raw8686step0 line 317
  62. def OAI.MUB6.Certificate.PairSemantics.raw8686step1 line 319
  63. def OAI.MUB6.Certificate.PairSemantics.raw8686step2 line 321
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8686 line 323
  65. def OAI.MUB6.Certificate.PairSemantics.raw8687 line 341
  66. def OAI.MUB6.Certificate.PairSemantics.raw8687step0 line 343
  67. def OAI.MUB6.Certificate.PairSemantics.raw8687step1 line 345
  68. def OAI.MUB6.Certificate.PairSemantics.raw8687step2 line 347
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8687 line 349
  70. def OAI.MUB6.Certificate.PairSemantics.raw8688 line 367
  71. def OAI.MUB6.Certificate.PairSemantics.raw8688step0 line 369
  72. def OAI.MUB6.Certificate.PairSemantics.raw8688step1 line 371
  73. def OAI.MUB6.Certificate.PairSemantics.raw8688step2 line 373
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical8688 line 375
  75. def OAI.MUB6.Certificate.PairSemantics.raw8689 line 393
  76. def OAI.MUB6.Certificate.PairSemantics.raw8689step0 line 395
  77. def OAI.MUB6.Certificate.PairSemantics.raw8689step1 line 397
  78. def OAI.MUB6.Certificate.PairSemantics.raw8689step2 line 399
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8689 line 401
  80. def OAI.MUB6.Certificate.PairSemantics.raw8690 line 419
  81. def OAI.MUB6.Certificate.PairSemantics.raw8690step0 line 421
  82. def OAI.MUB6.Certificate.PairSemantics.raw8690step1 line 423
  83. def OAI.MUB6.Certificate.PairSemantics.raw8690step2 line 425
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8690 line 427
  85. def OAI.MUB6.Certificate.PairSemantics.raw8691 line 445
  86. def OAI.MUB6.Certificate.PairSemantics.raw8691step0 line 447
  87. def OAI.MUB6.Certificate.PairSemantics.raw8691step1 line 449
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8691 line 451
  89. def OAI.MUB6.Certificate.PairSemantics.raw8692 line 465
  90. def OAI.MUB6.Certificate.PairSemantics.raw8692step0 line 467
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8692 line 469
  92. def OAI.MUB6.Certificate.PairSemantics.raw8693 line 478
  93. def OAI.MUB6.Certificate.PairSemantics.raw8693step0 line 480
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8693 line 482
  95. def OAI.MUB6.Certificate.PairSemantics.raw8694 line 491
  96. def OAI.MUB6.Certificate.PairSemantics.raw8694step0 line 493
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical8694 line 495
  98. def OAI.MUB6.Certificate.PairSemantics.raw8695 line 504
  99. def OAI.MUB6.Certificate.PairSemantics.raw8695step0 line 506
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical8695 line 508
  101. def OAI.MUB6.Certificate.PairSemantics.raw8696 line 517
  102. def OAI.MUB6.Certificate.PairSemantics.raw8696step0 line 519
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical8696 line 521
  104. def OAI.MUB6.Certificate.PairSemantics.raw8697 line 530
  105. def OAI.MUB6.Certificate.PairSemantics.raw8697step0 line 532
  106. def OAI.MUB6.Certificate.PairSemantics.raw8697step1 line 534
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8697 line 536
  108. def OAI.MUB6.Certificate.PairSemantics.raw8698 line 551
  109. def OAI.MUB6.Certificate.PairSemantics.raw8698step0 line 553
  110. def OAI.MUB6.Certificate.PairSemantics.raw8698step1 line 555
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8698 line 557
  112. def OAI.MUB6.Certificate.PairSemantics.raw8699 line 571
  113. def OAI.MUB6.Certificate.PairSemantics.raw8699step0 line 573
  114. def OAI.MUB6.Certificate.PairSemantics.raw8699step1 line 575
  115. def OAI.MUB6.Certificate.PairSemantics.raw8699step2 line 577
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical8699 line 579
  117. def OAI.MUB6.Certificate.PairSemantics.raw8700 line 597
  118. def OAI.MUB6.Certificate.PairSemantics.raw8700step0 line 599
  119. def OAI.MUB6.Certificate.PairSemantics.raw8700step1 line 601
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8700 line 603
  121. def OAI.MUB6.Certificate.PairSemantics.raw8701 line 617
  122. def OAI.MUB6.Certificate.PairSemantics.raw8701step0 line 619
  123. def OAI.MUB6.Certificate.PairSemantics.raw8701step1 line 621
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical8701 line 623
  125. def OAI.MUB6.Certificate.PairSemantics.raw8702 line 637
  126. def OAI.MUB6.Certificate.PairSemantics.raw8702step0 line 639
  127. def OAI.MUB6.Certificate.PairSemantics.raw8702step1 line 641
  128. def OAI.MUB6.Certificate.PairSemantics.raw8702step2 line 643
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical8702 line 645
  130. def OAI.MUB6.Certificate.PairSemantics.raw8703 line 663
  131. def OAI.MUB6.Certificate.PairSemantics.raw8703step0 line 665
  132. def OAI.MUB6.Certificate.PairSemantics.raw8703step1 line 667
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical8703 line 669