OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical181.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5792 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw5792step0 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw5792step1 line 16
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5792 line 18
  5. def OAI.MUB6.Certificate.PairSemantics.raw5793 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw5793step0 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw5793step1 line 35
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5793 line 37
  9. def OAI.MUB6.Certificate.PairSemantics.raw5794 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw5794step0 line 52
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5794 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw5795 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw5795step0 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw5795step1 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5795 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw5796 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw5796step0 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw5796step1 line 86
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5796 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw5797 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw5797step0 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw5797step1 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw5797step2 line 107
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5797 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw5798 line 126
  26. def OAI.MUB6.Certificate.PairSemantics.raw5798step0 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw5798step1 line 130
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5798 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw5799 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw5799step0 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw5799step1 line 149
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5799 line 151
  33. def OAI.MUB6.Certificate.PairSemantics.raw5800 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw5800step0 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw5800step1 line 168
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5800 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw5801 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw5801step0 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw5801step1 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5801 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw5802 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw5802step0 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw5802step1 line 206
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5802 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw5803 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw5803step0 line 223
  47. def OAI.MUB6.Certificate.PairSemantics.raw5803step1 line 225
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5803 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw5804 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw5804step0 line 242
  51. def OAI.MUB6.Certificate.PairSemantics.raw5804step1 line 244
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5804 line 246
  53. def OAI.MUB6.Certificate.PairSemantics.raw5805 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw5805step0 line 261
  55. def OAI.MUB6.Certificate.PairSemantics.raw5805step1 line 263
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5805 line 265
  57. def OAI.MUB6.Certificate.PairSemantics.raw5806 line 278
  58. def OAI.MUB6.Certificate.PairSemantics.raw5806step0 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw5806step1 line 282
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5806 line 284
  61. def OAI.MUB6.Certificate.PairSemantics.raw5807 line 297
  62. def OAI.MUB6.Certificate.PairSemantics.raw5807step0 line 299
  63. def OAI.MUB6.Certificate.PairSemantics.raw5807step1 line 301
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5807 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw5808 line 316
  66. def OAI.MUB6.Certificate.PairSemantics.raw5808step0 line 318
  67. def OAI.MUB6.Certificate.PairSemantics.raw5808step1 line 320
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5808 line 322
  69. def OAI.MUB6.Certificate.PairSemantics.raw5809 line 335
  70. def OAI.MUB6.Certificate.PairSemantics.raw5809step0 line 337
  71. def OAI.MUB6.Certificate.PairSemantics.raw5809step1 line 339
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5809 line 341
  73. def OAI.MUB6.Certificate.PairSemantics.raw5810 line 354
  74. def OAI.MUB6.Certificate.PairSemantics.raw5810step0 line 356
  75. def OAI.MUB6.Certificate.PairSemantics.raw5810step1 line 358
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5810 line 360
  77. def OAI.MUB6.Certificate.PairSemantics.raw5811 line 373
  78. def OAI.MUB6.Certificate.PairSemantics.raw5811step0 line 375
  79. def OAI.MUB6.Certificate.PairSemantics.raw5811step1 line 377
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5811 line 379
  81. def OAI.MUB6.Certificate.PairSemantics.raw5812 line 392
  82. def OAI.MUB6.Certificate.PairSemantics.raw5812step0 line 394
  83. def OAI.MUB6.Certificate.PairSemantics.raw5812step1 line 396
  84. def OAI.MUB6.Certificate.PairSemantics.raw5812step2 line 398
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5812 line 400
  86. def OAI.MUB6.Certificate.PairSemantics.raw5813 line 417
  87. def OAI.MUB6.Certificate.PairSemantics.raw5813step0 line 419
  88. def OAI.MUB6.Certificate.PairSemantics.raw5813step1 line 421
  89. def OAI.MUB6.Certificate.PairSemantics.raw5813step2 line 423
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical5813 line 425
  91. def OAI.MUB6.Certificate.PairSemantics.raw5814 line 442
  92. def OAI.MUB6.Certificate.PairSemantics.raw5814step0 line 444
  93. def OAI.MUB6.Certificate.PairSemantics.raw5814step1 line 446
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical5814 line 448
  95. def OAI.MUB6.Certificate.PairSemantics.raw5815 line 461
  96. def OAI.MUB6.Certificate.PairSemantics.raw5815step0 line 463
  97. def OAI.MUB6.Certificate.PairSemantics.raw5815step1 line 465
  98. def OAI.MUB6.Certificate.PairSemantics.raw5815step2 line 467
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5815 line 469
  100. def OAI.MUB6.Certificate.PairSemantics.raw5816 line 486
  101. def OAI.MUB6.Certificate.PairSemantics.raw5816step0 line 488
  102. def OAI.MUB6.Certificate.PairSemantics.raw5816step1 line 490
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5816 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw5817 line 505
  105. def OAI.MUB6.Certificate.PairSemantics.raw5817step0 line 507
  106. def OAI.MUB6.Certificate.PairSemantics.raw5817step1 line 509
  107. def OAI.MUB6.Certificate.PairSemantics.raw5817step2 line 511
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical5817 line 513
  109. def OAI.MUB6.Certificate.PairSemantics.raw5818 line 530
  110. def OAI.MUB6.Certificate.PairSemantics.raw5818step0 line 532
  111. def OAI.MUB6.Certificate.PairSemantics.raw5818step1 line 534
  112. def OAI.MUB6.Certificate.PairSemantics.raw5818step2 line 536
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical5818 line 538
  114. def OAI.MUB6.Certificate.PairSemantics.raw5819 line 555
  115. def OAI.MUB6.Certificate.PairSemantics.raw5819step0 line 557
  116. def OAI.MUB6.Certificate.PairSemantics.raw5819step1 line 559
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical5819 line 561
  118. def OAI.MUB6.Certificate.PairSemantics.raw5820 line 574
  119. def OAI.MUB6.Certificate.PairSemantics.raw5820step0 line 576
  120. def OAI.MUB6.Certificate.PairSemantics.raw5820step1 line 578
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical5820 line 580
  122. def OAI.MUB6.Certificate.PairSemantics.raw5821 line 593
  123. def OAI.MUB6.Certificate.PairSemantics.raw5821step0 line 595
  124. def OAI.MUB6.Certificate.PairSemantics.raw5821step1 line 597
  125. def OAI.MUB6.Certificate.PairSemantics.raw5821step2 line 599
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical5821 line 601
  127. def OAI.MUB6.Certificate.PairSemantics.raw5822 line 618
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical5822 line 620
  129. def OAI.MUB6.Certificate.PairSemantics.raw5823 line 624
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical5823 line 626