OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical247.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7904 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw7904step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw7904step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7904 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw7905 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw7905step0 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw7905step1 line 38
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7905 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw7906 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw7906step0 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw7906step1 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw7906step2 line 59
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7906 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw7907 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw7907step0 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw7907step1 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7907 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw7908 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw7908step0 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw7908step1 line 101
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7908 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw7909 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw7909step0 line 118
  24. def OAI.MUB6.Certificate.PairSemantics.raw7909step1 line 120
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7909 line 122
  26. def OAI.MUB6.Certificate.PairSemantics.raw7910 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw7910step0 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw7910step1 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw7910step2 line 141
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7910 line 143
  31. def OAI.MUB6.Certificate.PairSemantics.raw7911 line 160
  32. def OAI.MUB6.Certificate.PairSemantics.raw7911step0 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw7911step1 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw7911step2 line 166
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7911 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw7912 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw7912step0 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw7912step1 line 189
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7912 line 191
  40. def OAI.MUB6.Certificate.PairSemantics.raw7913 line 204
  41. def OAI.MUB6.Certificate.PairSemantics.raw7913step0 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw7913step1 line 208
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7913 line 210
  44. def OAI.MUB6.Certificate.PairSemantics.raw7914 line 223
  45. def OAI.MUB6.Certificate.PairSemantics.raw7914step0 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw7914step1 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw7914step2 line 229
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7914 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw7915 line 248
  50. def OAI.MUB6.Certificate.PairSemantics.raw7915step0 line 250
  51. def OAI.MUB6.Certificate.PairSemantics.raw7915step1 line 252
  52. def OAI.MUB6.Certificate.PairSemantics.raw7915step2 line 254
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical7915 line 256
  54. def OAI.MUB6.Certificate.PairSemantics.raw7916 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw7916step0 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw7916step1 line 277
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7916 line 279
  58. def OAI.MUB6.Certificate.PairSemantics.raw7917 line 292
  59. def OAI.MUB6.Certificate.PairSemantics.raw7917step0 line 294
  60. def OAI.MUB6.Certificate.PairSemantics.raw7917step1 line 296
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7917 line 298
  62. def OAI.MUB6.Certificate.PairSemantics.raw7918 line 311
  63. def OAI.MUB6.Certificate.PairSemantics.raw7918step0 line 313
  64. def OAI.MUB6.Certificate.PairSemantics.raw7918step1 line 315
  65. def OAI.MUB6.Certificate.PairSemantics.raw7918step2 line 317
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7918 line 319
  67. def OAI.MUB6.Certificate.PairSemantics.raw7919 line 336
  68. def OAI.MUB6.Certificate.PairSemantics.raw7919step0 line 338
  69. def OAI.MUB6.Certificate.PairSemantics.raw7919step1 line 340
  70. def OAI.MUB6.Certificate.PairSemantics.raw7919step2 line 342
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7919 line 344
  72. def OAI.MUB6.Certificate.PairSemantics.raw7920 line 361
  73. def OAI.MUB6.Certificate.PairSemantics.raw7920step0 line 363
  74. def OAI.MUB6.Certificate.PairSemantics.raw7920step1 line 365
  75. def OAI.MUB6.Certificate.PairSemantics.raw7920step2 line 367
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7920 line 369
  77. def OAI.MUB6.Certificate.PairSemantics.raw7921 line 386
  78. def OAI.MUB6.Certificate.PairSemantics.raw7921step0 line 388
  79. def OAI.MUB6.Certificate.PairSemantics.raw7921step1 line 390
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7921 line 392
  81. def OAI.MUB6.Certificate.PairSemantics.raw7922 line 405
  82. def OAI.MUB6.Certificate.PairSemantics.raw7922step0 line 407
  83. def OAI.MUB6.Certificate.PairSemantics.raw7922step1 line 409
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7922 line 411
  85. def OAI.MUB6.Certificate.PairSemantics.raw7923 line 424
  86. def OAI.MUB6.Certificate.PairSemantics.raw7923step0 line 426
  87. def OAI.MUB6.Certificate.PairSemantics.raw7923step1 line 428
  88. def OAI.MUB6.Certificate.PairSemantics.raw7923step2 line 430
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7923 line 432
  90. def OAI.MUB6.Certificate.PairSemantics.raw7924 line 449
  91. def OAI.MUB6.Certificate.PairSemantics.raw7924step0 line 451
  92. def OAI.MUB6.Certificate.PairSemantics.raw7924step1 line 453
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7924 line 455
  94. def OAI.MUB6.Certificate.PairSemantics.raw7925 line 468
  95. def OAI.MUB6.Certificate.PairSemantics.raw7925step0 line 470
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7925 line 472
  97. def OAI.MUB6.Certificate.PairSemantics.raw7926 line 481
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7926 line 483
  99. def OAI.MUB6.Certificate.PairSemantics.raw7927 line 487
  100. def OAI.MUB6.Certificate.PairSemantics.raw7927step0 line 489
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7927 line 491
  102. def OAI.MUB6.Certificate.PairSemantics.raw7928 line 500
  103. def OAI.MUB6.Certificate.PairSemantics.raw7928step0 line 502
  104. def OAI.MUB6.Certificate.PairSemantics.raw7928step1 line 504
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7928 line 506
  106. def OAI.MUB6.Certificate.PairSemantics.raw7929 line 519
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7929 line 521
  108. def OAI.MUB6.Certificate.PairSemantics.raw7930 line 525
  109. def OAI.MUB6.Certificate.PairSemantics.raw7930step0 line 527
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical7930 line 529
  111. def OAI.MUB6.Certificate.PairSemantics.raw7931 line 538
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7931 line 540
  113. def OAI.MUB6.Certificate.PairSemantics.raw7932 line 544
  114. def OAI.MUB6.Certificate.PairSemantics.raw7932step0 line 546
  115. def OAI.MUB6.Certificate.PairSemantics.raw7932step1 line 548
  116. def OAI.MUB6.Certificate.PairSemantics.raw7932step2 line 550
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical7932 line 552
  118. def OAI.MUB6.Certificate.PairSemantics.raw7933 line 570
  119. def OAI.MUB6.Certificate.PairSemantics.raw7933step0 line 572
  120. def OAI.MUB6.Certificate.PairSemantics.raw7933step1 line 574
  121. def OAI.MUB6.Certificate.PairSemantics.raw7933step2 line 576
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical7933 line 578
  123. def OAI.MUB6.Certificate.PairSemantics.raw7934 line 596
  124. def OAI.MUB6.Certificate.PairSemantics.raw7934step0 line 598
  125. def OAI.MUB6.Certificate.PairSemantics.raw7934step1 line 600
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical7934 line 602
  127. def OAI.MUB6.Certificate.PairSemantics.raw7935 line 615
  128. def OAI.MUB6.Certificate.PairSemantics.raw7935step0 line 617
  129. def OAI.MUB6.Certificate.PairSemantics.raw7935step1 line 619
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical7935 line 621