OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical205.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6560 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw6560step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw6560step1 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw6560step2 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6560 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw6561 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw6561step0 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw6561step1 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw6561step2 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6561 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw6562 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw6562step0 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw6562step1 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw6562step2 line 71
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6562 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw6563 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw6563step0 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw6563step1 line 94
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6563 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw6564 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw6564step0 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw6564step1 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw6564step2 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6564 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw6565 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw6565step0 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw6565step1 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw6565step2 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6565 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw6566 line 159
  31. def OAI.MUB6.Certificate.PairSemantics.raw6566step0 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw6566step1 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw6566step2 line 165
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6566 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw6567 line 184
  36. def OAI.MUB6.Certificate.PairSemantics.raw6567step0 line 186
  37. def OAI.MUB6.Certificate.PairSemantics.raw6567step1 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw6567step2 line 190
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6567 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw6568 line 209
  41. def OAI.MUB6.Certificate.PairSemantics.raw6568step0 line 211
  42. def OAI.MUB6.Certificate.PairSemantics.raw6568step1 line 213
  43. def OAI.MUB6.Certificate.PairSemantics.raw6568step2 line 215
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6568 line 217
  45. def OAI.MUB6.Certificate.PairSemantics.raw6569 line 234
  46. def OAI.MUB6.Certificate.PairSemantics.raw6569step0 line 236
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6569 line 238
  48. def OAI.MUB6.Certificate.PairSemantics.raw6570 line 247
  49. def OAI.MUB6.Certificate.PairSemantics.raw6570step0 line 249
  50. def OAI.MUB6.Certificate.PairSemantics.raw6570step1 line 251
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6570 line 253
  52. def OAI.MUB6.Certificate.PairSemantics.raw6571 line 266
  53. def OAI.MUB6.Certificate.PairSemantics.raw6571step0 line 268
  54. def OAI.MUB6.Certificate.PairSemantics.raw6571step1 line 270
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6571 line 272
  56. def OAI.MUB6.Certificate.PairSemantics.raw6572 line 285
  57. def OAI.MUB6.Certificate.PairSemantics.raw6572step0 line 287
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6572 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw6573 line 298
  60. def OAI.MUB6.Certificate.PairSemantics.raw6573step0 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw6573step1 line 302
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6573 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw6574 line 317
  64. def OAI.MUB6.Certificate.PairSemantics.raw6574step0 line 319
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6574 line 321
  66. def OAI.MUB6.Certificate.PairSemantics.raw6575 line 330
  67. def OAI.MUB6.Certificate.PairSemantics.raw6575step0 line 332
  68. def OAI.MUB6.Certificate.PairSemantics.raw6575step1 line 334
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6575 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw6576 line 349
  71. def OAI.MUB6.Certificate.PairSemantics.raw6576step0 line 351
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6576 line 353
  73. def OAI.MUB6.Certificate.PairSemantics.raw6577 line 362
  74. def OAI.MUB6.Certificate.PairSemantics.raw6577step0 line 364
  75. def OAI.MUB6.Certificate.PairSemantics.raw6577step1 line 366
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6577 line 368
  77. def OAI.MUB6.Certificate.PairSemantics.raw6578 line 381
  78. def OAI.MUB6.Certificate.PairSemantics.raw6578step0 line 383
  79. def OAI.MUB6.Certificate.PairSemantics.raw6578step1 line 385
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6578 line 387
  81. def OAI.MUB6.Certificate.PairSemantics.raw6579 line 400
  82. def OAI.MUB6.Certificate.PairSemantics.raw6579step0 line 402
  83. def OAI.MUB6.Certificate.PairSemantics.raw6579step1 line 404
  84. def OAI.MUB6.Certificate.PairSemantics.raw6579step2 line 406
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6579 line 408
  86. def OAI.MUB6.Certificate.PairSemantics.raw6580 line 425
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical6580 line 427
  88. def OAI.MUB6.Certificate.PairSemantics.raw6581 line 431
  89. def OAI.MUB6.Certificate.PairSemantics.raw6581step0 line 433
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6581 line 435
  91. def OAI.MUB6.Certificate.PairSemantics.raw6582 line 444
  92. def OAI.MUB6.Certificate.PairSemantics.raw6582step0 line 446
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6582 line 448
  94. def OAI.MUB6.Certificate.PairSemantics.raw6583 line 457
  95. def OAI.MUB6.Certificate.PairSemantics.raw6583step0 line 459
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical6583 line 461
  97. def OAI.MUB6.Certificate.PairSemantics.raw6584 line 470
  98. def OAI.MUB6.Certificate.PairSemantics.raw6584step0 line 472
  99. def OAI.MUB6.Certificate.PairSemantics.raw6584step1 line 474
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical6584 line 476
  101. def OAI.MUB6.Certificate.PairSemantics.raw6585 line 489
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical6585 line 491
  103. def OAI.MUB6.Certificate.PairSemantics.raw6586 line 495
  104. def OAI.MUB6.Certificate.PairSemantics.raw6586step0 line 497
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical6586 line 499
  106. def OAI.MUB6.Certificate.PairSemantics.raw6587 line 508
  107. def OAI.MUB6.Certificate.PairSemantics.raw6587step0 line 510
  108. def OAI.MUB6.Certificate.PairSemantics.raw6587step1 line 512
  109. def OAI.MUB6.Certificate.PairSemantics.raw6587step2 line 514
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical6587 line 516
  111. def OAI.MUB6.Certificate.PairSemantics.raw6588 line 533
  112. def OAI.MUB6.Certificate.PairSemantics.raw6588step0 line 535
  113. def OAI.MUB6.Certificate.PairSemantics.raw6588step1 line 537
  114. def OAI.MUB6.Certificate.PairSemantics.raw6588step2 line 539
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical6588 line 541
  116. def OAI.MUB6.Certificate.PairSemantics.raw6589 line 558
  117. def OAI.MUB6.Certificate.PairSemantics.raw6589step0 line 560
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical6589 line 562
  119. def OAI.MUB6.Certificate.PairSemantics.raw6590 line 571
  120. def OAI.MUB6.Certificate.PairSemantics.raw6590step0 line 573
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical6590 line 575
  122. def OAI.MUB6.Certificate.PairSemantics.raw6591 line 584
  123. def OAI.MUB6.Certificate.PairSemantics.raw6591step0 line 586
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical6591 line 588