OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical311.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9952 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw9952step0 line 12
  3. def OAI.MUB6.Certificate.PairSemantics.raw9952step1 line 14
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9952 line 16
  5. def OAI.MUB6.Certificate.PairSemantics.raw9953 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw9953step0 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw9953step1 line 33
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9953 line 35
  9. def OAI.MUB6.Certificate.PairSemantics.raw9954 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw9954step0 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw9954step1 line 52
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9954 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw9955 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw9955step0 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw9955step1 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw9955step2 line 73
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9955 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw9956 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw9956step0 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw9956step1 line 96
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9956 line 98
  22. def OAI.MUB6.Certificate.PairSemantics.raw9957 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw9957step0 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw9957step1 line 115
  25. def OAI.MUB6.Certificate.PairSemantics.raw9957step2 line 117
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9957 line 119
  27. def OAI.MUB6.Certificate.PairSemantics.raw9958 line 136
  28. def OAI.MUB6.Certificate.PairSemantics.raw9958step0 line 138
  29. def OAI.MUB6.Certificate.PairSemantics.raw9958step1 line 140
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9958 line 142
  31. def OAI.MUB6.Certificate.PairSemantics.raw9959 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw9959step0 line 157
  33. def OAI.MUB6.Certificate.PairSemantics.raw9959step1 line 159
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9959 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw9960 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw9960step0 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw9960step1 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw9960step2 line 180
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9960 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw9961 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw9961step0 line 201
  42. def OAI.MUB6.Certificate.PairSemantics.raw9961step1 line 203
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9961 line 205
  44. def OAI.MUB6.Certificate.PairSemantics.raw9962 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw9962step0 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw9962step1 line 222
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9962 line 224
  48. def OAI.MUB6.Certificate.PairSemantics.raw9963 line 237
  49. def OAI.MUB6.Certificate.PairSemantics.raw9963step0 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw9963step1 line 241
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical9963 line 243
  52. def OAI.MUB6.Certificate.PairSemantics.raw9964 line 256
  53. def OAI.MUB6.Certificate.PairSemantics.raw9964step0 line 258
  54. def OAI.MUB6.Certificate.PairSemantics.raw9964step1 line 260
  55. def OAI.MUB6.Certificate.PairSemantics.raw9964step2 line 262
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9964 line 264
  57. def OAI.MUB6.Certificate.PairSemantics.raw9965 line 281
  58. def OAI.MUB6.Certificate.PairSemantics.raw9965step0 line 283
  59. def OAI.MUB6.Certificate.PairSemantics.raw9965step1 line 285
  60. def OAI.MUB6.Certificate.PairSemantics.raw9965step2 line 287
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9965 line 289
  62. def OAI.MUB6.Certificate.PairSemantics.raw9966 line 306
  63. def OAI.MUB6.Certificate.PairSemantics.raw9966step0 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw9966step1 line 310
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9966 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw9967 line 325
  67. def OAI.MUB6.Certificate.PairSemantics.raw9967step0 line 327
  68. def OAI.MUB6.Certificate.PairSemantics.raw9967step1 line 329
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9967 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw9968 line 344
  71. def OAI.MUB6.Certificate.PairSemantics.raw9968step0 line 346
  72. def OAI.MUB6.Certificate.PairSemantics.raw9968step1 line 348
  73. def OAI.MUB6.Certificate.PairSemantics.raw9968step2 line 350
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9968 line 352
  75. def OAI.MUB6.Certificate.PairSemantics.raw9969 line 369
  76. def OAI.MUB6.Certificate.PairSemantics.raw9969step0 line 371
  77. def OAI.MUB6.Certificate.PairSemantics.raw9969step1 line 373
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9969 line 375
  79. def OAI.MUB6.Certificate.PairSemantics.raw9970 line 388
  80. def OAI.MUB6.Certificate.PairSemantics.raw9970step0 line 390
  81. def OAI.MUB6.Certificate.PairSemantics.raw9970step1 line 392
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9970 line 394
  83. def OAI.MUB6.Certificate.PairSemantics.raw9971 line 407
  84. def OAI.MUB6.Certificate.PairSemantics.raw9971step0 line 409
  85. def OAI.MUB6.Certificate.PairSemantics.raw9971step1 line 411
  86. def OAI.MUB6.Certificate.PairSemantics.raw9971step2 line 413
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9971 line 415
  88. def OAI.MUB6.Certificate.PairSemantics.raw9972 line 432
  89. def OAI.MUB6.Certificate.PairSemantics.raw9972step0 line 434
  90. def OAI.MUB6.Certificate.PairSemantics.raw9972step1 line 436
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9972 line 438
  92. def OAI.MUB6.Certificate.PairSemantics.raw9973 line 451
  93. def OAI.MUB6.Certificate.PairSemantics.raw9973step0 line 453
  94. def OAI.MUB6.Certificate.PairSemantics.raw9973step1 line 455
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9973 line 457
  96. def OAI.MUB6.Certificate.PairSemantics.raw9974 line 470
  97. def OAI.MUB6.Certificate.PairSemantics.raw9974step0 line 472
  98. def OAI.MUB6.Certificate.PairSemantics.raw9974step1 line 474
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9974 line 476
  100. def OAI.MUB6.Certificate.PairSemantics.raw9975 line 489
  101. def OAI.MUB6.Certificate.PairSemantics.raw9975step0 line 491
  102. def OAI.MUB6.Certificate.PairSemantics.raw9975step1 line 493
  103. def OAI.MUB6.Certificate.PairSemantics.raw9975step2 line 495
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical9975 line 497
  105. def OAI.MUB6.Certificate.PairSemantics.raw9976 line 514
  106. def OAI.MUB6.Certificate.PairSemantics.raw9976step0 line 516
  107. def OAI.MUB6.Certificate.PairSemantics.raw9976step1 line 518
  108. def OAI.MUB6.Certificate.PairSemantics.raw9976step2 line 520
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9976 line 522
  110. def OAI.MUB6.Certificate.PairSemantics.raw9977 line 539
  111. def OAI.MUB6.Certificate.PairSemantics.raw9977step0 line 541
  112. def OAI.MUB6.Certificate.PairSemantics.raw9977step1 line 543
  113. def OAI.MUB6.Certificate.PairSemantics.raw9977step2 line 545
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical9977 line 547
  115. def OAI.MUB6.Certificate.PairSemantics.raw9978 line 564
  116. def OAI.MUB6.Certificate.PairSemantics.raw9978step0 line 566
  117. def OAI.MUB6.Certificate.PairSemantics.raw9978step1 line 568
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical9978 line 570
  119. def OAI.MUB6.Certificate.PairSemantics.raw9979 line 583
  120. def OAI.MUB6.Certificate.PairSemantics.raw9979step0 line 585
  121. def OAI.MUB6.Certificate.PairSemantics.raw9979step1 line 587
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical9979 line 589
  123. def OAI.MUB6.Certificate.PairSemantics.raw9980 line 602
  124. def OAI.MUB6.Certificate.PairSemantics.raw9980step0 line 604
  125. def OAI.MUB6.Certificate.PairSemantics.raw9980step1 line 606
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical9980 line 608
  127. def OAI.MUB6.Certificate.PairSemantics.raw9981 line 621
  128. def OAI.MUB6.Certificate.PairSemantics.raw9981step0 line 623
  129. def OAI.MUB6.Certificate.PairSemantics.raw9981step1 line 625
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical9981 line 627
  131. def OAI.MUB6.Certificate.PairSemantics.raw9982 line 640
  132. def OAI.MUB6.Certificate.PairSemantics.raw9982step0 line 642
  133. def OAI.MUB6.Certificate.PairSemantics.raw9982step1 line 644
  134. theorem OAI.MUB6.Certificate.PairSemantics.canonical9982 line 646
  135. def OAI.MUB6.Certificate.PairSemantics.raw9983 line 659
  136. def OAI.MUB6.Certificate.PairSemantics.raw9983step0 line 661
  137. def OAI.MUB6.Certificate.PairSemantics.raw9983step1 line 663
  138. def OAI.MUB6.Certificate.PairSemantics.raw9983step2 line 665
  139. theorem OAI.MUB6.Certificate.PairSemantics.canonical9983 line 667