OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical0.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw0 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw0step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw0step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical0 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw1 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw1step0 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw1step1 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw2 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw2step0 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw2step1 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw3 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw3step0 line 73
  15. def OAI.MUB6.Certificate.PairSemantics.raw3step1 line 75
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3 line 77
  17. def OAI.MUB6.Certificate.PairSemantics.raw4 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw4step0 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw4step1 line 94
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4 line 96
  21. def OAI.MUB6.Certificate.PairSemantics.raw5 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw5step0 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw5step1 line 113
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5 line 115
  25. def OAI.MUB6.Certificate.PairSemantics.raw6 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw6step0 line 130
  27. def OAI.MUB6.Certificate.PairSemantics.raw6step1 line 132
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6 line 134
  29. def OAI.MUB6.Certificate.PairSemantics.raw7 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw7step0 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw7step1 line 151
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw8 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw8step0 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw8step1 line 170
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical8 line 172
  37. def OAI.MUB6.Certificate.PairSemantics.raw9 line 185
  38. def OAI.MUB6.Certificate.PairSemantics.raw9step0 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw9step1 line 189
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw10 line 204
  42. def OAI.MUB6.Certificate.PairSemantics.raw10step0 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw10step1 line 208
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical10 line 210
  45. def OAI.MUB6.Certificate.PairSemantics.raw11 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw11step0 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw11step1 line 227
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical11 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw12 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw12step0 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw12step1 line 246
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical12 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw13 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw13step0 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw13step1 line 265
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical13 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw14 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw14step0 line 282
  59. def OAI.MUB6.Certificate.PairSemantics.raw14step1 line 284
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical14 line 286
  61. def OAI.MUB6.Certificate.PairSemantics.raw15 line 299
  62. def OAI.MUB6.Certificate.PairSemantics.raw15step0 line 301
  63. def OAI.MUB6.Certificate.PairSemantics.raw15step1 line 303
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical15 line 305
  65. def OAI.MUB6.Certificate.PairSemantics.raw16 line 318
  66. def OAI.MUB6.Certificate.PairSemantics.raw16step0 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw16step1 line 322
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical16 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw17 line 337
  70. def OAI.MUB6.Certificate.PairSemantics.raw17step0 line 339
  71. def OAI.MUB6.Certificate.PairSemantics.raw17step1 line 341
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical17 line 343
  73. def OAI.MUB6.Certificate.PairSemantics.raw18 line 356
  74. def OAI.MUB6.Certificate.PairSemantics.raw18step0 line 358
  75. def OAI.MUB6.Certificate.PairSemantics.raw18step1 line 360
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical18 line 362
  77. def OAI.MUB6.Certificate.PairSemantics.raw19 line 375
  78. def OAI.MUB6.Certificate.PairSemantics.raw19step0 line 377
  79. def OAI.MUB6.Certificate.PairSemantics.raw19step1 line 379
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical19 line 381
  81. def OAI.MUB6.Certificate.PairSemantics.raw20 line 394
  82. def OAI.MUB6.Certificate.PairSemantics.raw20step0 line 396
  83. def OAI.MUB6.Certificate.PairSemantics.raw20step1 line 398
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical20 line 400
  85. def OAI.MUB6.Certificate.PairSemantics.raw21 line 413
  86. def OAI.MUB6.Certificate.PairSemantics.raw21step0 line 415
  87. def OAI.MUB6.Certificate.PairSemantics.raw21step1 line 417
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical21 line 419
  89. def OAI.MUB6.Certificate.PairSemantics.raw22 line 432
  90. def OAI.MUB6.Certificate.PairSemantics.raw22step0 line 434
  91. def OAI.MUB6.Certificate.PairSemantics.raw22step1 line 436
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical22 line 438
  93. def OAI.MUB6.Certificate.PairSemantics.raw23 line 451
  94. def OAI.MUB6.Certificate.PairSemantics.raw23step0 line 453
  95. def OAI.MUB6.Certificate.PairSemantics.raw23step1 line 455
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical23 line 457
  97. def OAI.MUB6.Certificate.PairSemantics.raw24 line 470
  98. def OAI.MUB6.Certificate.PairSemantics.raw24step0 line 472
  99. def OAI.MUB6.Certificate.PairSemantics.raw24step1 line 474
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical24 line 476
  101. def OAI.MUB6.Certificate.PairSemantics.raw25 line 489
  102. def OAI.MUB6.Certificate.PairSemantics.raw25step0 line 491
  103. def OAI.MUB6.Certificate.PairSemantics.raw25step1 line 493
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical25 line 495
  105. def OAI.MUB6.Certificate.PairSemantics.raw26 line 508
  106. def OAI.MUB6.Certificate.PairSemantics.raw26step0 line 510
  107. def OAI.MUB6.Certificate.PairSemantics.raw26step1 line 512
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical26 line 514
  109. def OAI.MUB6.Certificate.PairSemantics.raw27 line 527
  110. def OAI.MUB6.Certificate.PairSemantics.raw27step0 line 529
  111. def OAI.MUB6.Certificate.PairSemantics.raw27step1 line 531
  112. def OAI.MUB6.Certificate.PairSemantics.raw27step2 line 533
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical27 line 535
  114. def OAI.MUB6.Certificate.PairSemantics.raw28 line 552
  115. def OAI.MUB6.Certificate.PairSemantics.raw28step0 line 554
  116. def OAI.MUB6.Certificate.PairSemantics.raw28step1 line 556
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical28 line 558
  118. def OAI.MUB6.Certificate.PairSemantics.raw29 line 571
  119. def OAI.MUB6.Certificate.PairSemantics.raw29step0 line 573
  120. def OAI.MUB6.Certificate.PairSemantics.raw29step1 line 575
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical29 line 577
  122. def OAI.MUB6.Certificate.PairSemantics.raw30 line 590
  123. def OAI.MUB6.Certificate.PairSemantics.raw30step0 line 592
  124. def OAI.MUB6.Certificate.PairSemantics.raw30step1 line 594
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical30 line 596
  126. def OAI.MUB6.Certificate.PairSemantics.raw31 line 609
  127. def OAI.MUB6.Certificate.PairSemantics.raw31step0 line 611
  128. def OAI.MUB6.Certificate.PairSemantics.raw31step1 line 613
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical31 line 615