OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical252.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8064 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw8064step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw8064step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8064 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw8065 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw8065step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw8065step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8065 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw8066 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw8066step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw8066step1 line 64
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8066 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw8067 line 79
  14. def OAI.MUB6.Certificate.PairSemantics.raw8067step0 line 81
  15. def OAI.MUB6.Certificate.PairSemantics.raw8067step1 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw8067step2 line 85
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8067 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw8068 line 104
  19. def OAI.MUB6.Certificate.PairSemantics.raw8068step0 line 106
  20. def OAI.MUB6.Certificate.PairSemantics.raw8068step1 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw8068step2 line 110
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical8068 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw8069 line 129
  24. def OAI.MUB6.Certificate.PairSemantics.raw8069step0 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw8069step1 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw8069step2 line 135
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8069 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw8070 line 155
  29. def OAI.MUB6.Certificate.PairSemantics.raw8070step0 line 157
  30. def OAI.MUB6.Certificate.PairSemantics.raw8070step1 line 159
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8070 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw8071 line 174
  33. def OAI.MUB6.Certificate.PairSemantics.raw8071step0 line 176
  34. def OAI.MUB6.Certificate.PairSemantics.raw8071step1 line 178
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8071 line 180
  36. def OAI.MUB6.Certificate.PairSemantics.raw8072 line 193
  37. def OAI.MUB6.Certificate.PairSemantics.raw8072step0 line 195
  38. def OAI.MUB6.Certificate.PairSemantics.raw8072step1 line 197
  39. def OAI.MUB6.Certificate.PairSemantics.raw8072step2 line 199
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8072 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw8073 line 218
  42. def OAI.MUB6.Certificate.PairSemantics.raw8073step0 line 220
  43. def OAI.MUB6.Certificate.PairSemantics.raw8073step1 line 222
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8073 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw8074 line 237
  46. def OAI.MUB6.Certificate.PairSemantics.raw8074step0 line 239
  47. def OAI.MUB6.Certificate.PairSemantics.raw8074step1 line 241
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8074 line 243
  49. def OAI.MUB6.Certificate.PairSemantics.raw8075 line 256
  50. def OAI.MUB6.Certificate.PairSemantics.raw8075step0 line 258
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8075 line 260
  52. def OAI.MUB6.Certificate.PairSemantics.raw8076 line 269
  53. def OAI.MUB6.Certificate.PairSemantics.raw8076step0 line 271
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8076 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw8077 line 282
  56. def OAI.MUB6.Certificate.PairSemantics.raw8077step0 line 284
  57. def OAI.MUB6.Certificate.PairSemantics.raw8077step1 line 286
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8077 line 288
  59. def OAI.MUB6.Certificate.PairSemantics.raw8078 line 301
  60. def OAI.MUB6.Certificate.PairSemantics.raw8078step0 line 303
  61. def OAI.MUB6.Certificate.PairSemantics.raw8078step1 line 305
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8078 line 307
  63. def OAI.MUB6.Certificate.PairSemantics.raw8079 line 320
  64. def OAI.MUB6.Certificate.PairSemantics.raw8079step0 line 322
  65. def OAI.MUB6.Certificate.PairSemantics.raw8079step1 line 324
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8079 line 326
  67. def OAI.MUB6.Certificate.PairSemantics.raw8080 line 340
  68. def OAI.MUB6.Certificate.PairSemantics.raw8080step0 line 342
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8080 line 344
  70. def OAI.MUB6.Certificate.PairSemantics.raw8081 line 353
  71. def OAI.MUB6.Certificate.PairSemantics.raw8081step0 line 355
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8081 line 357
  73. def OAI.MUB6.Certificate.PairSemantics.raw8082 line 366
  74. def OAI.MUB6.Certificate.PairSemantics.raw8082step0 line 368
  75. def OAI.MUB6.Certificate.PairSemantics.raw8082step1 line 370
  76. def OAI.MUB6.Certificate.PairSemantics.raw8082step2 line 372
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8082 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw8083 line 392
  79. def OAI.MUB6.Certificate.PairSemantics.raw8083step0 line 394
  80. def OAI.MUB6.Certificate.PairSemantics.raw8083step1 line 396
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8083 line 398
  82. def OAI.MUB6.Certificate.PairSemantics.raw8084 line 411
  83. def OAI.MUB6.Certificate.PairSemantics.raw8084step0 line 413
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8084 line 415
  85. def OAI.MUB6.Certificate.PairSemantics.raw8085 line 424
  86. def OAI.MUB6.Certificate.PairSemantics.raw8085step0 line 426
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8085 line 428
  88. def OAI.MUB6.Certificate.PairSemantics.raw8086 line 437
  89. def OAI.MUB6.Certificate.PairSemantics.raw8086step0 line 439
  90. def OAI.MUB6.Certificate.PairSemantics.raw8086step1 line 441
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8086 line 443
  92. def OAI.MUB6.Certificate.PairSemantics.raw8087 line 456
  93. def OAI.MUB6.Certificate.PairSemantics.raw8087step0 line 458
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8087 line 460
  95. def OAI.MUB6.Certificate.PairSemantics.raw8088 line 469
  96. def OAI.MUB6.Certificate.PairSemantics.raw8088step0 line 471
  97. def OAI.MUB6.Certificate.PairSemantics.raw8088step1 line 473
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical8088 line 475
  99. def OAI.MUB6.Certificate.PairSemantics.raw8089 line 490
  100. def OAI.MUB6.Certificate.PairSemantics.raw8089step0 line 492
  101. def OAI.MUB6.Certificate.PairSemantics.raw8089step1 line 494
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8089 line 496
  103. def OAI.MUB6.Certificate.PairSemantics.raw8090 line 510
  104. def OAI.MUB6.Certificate.PairSemantics.raw8090step0 line 512
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical8090 line 514
  106. def OAI.MUB6.Certificate.PairSemantics.raw8091 line 523
  107. def OAI.MUB6.Certificate.PairSemantics.raw8091step0 line 525
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical8091 line 527
  109. def OAI.MUB6.Certificate.PairSemantics.raw8092 line 536
  110. def OAI.MUB6.Certificate.PairSemantics.raw8092step0 line 538
  111. def OAI.MUB6.Certificate.PairSemantics.raw8092step1 line 540
  112. def OAI.MUB6.Certificate.PairSemantics.raw8092step2 line 542
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical8092 line 544
  114. def OAI.MUB6.Certificate.PairSemantics.raw8093 line 563
  115. def OAI.MUB6.Certificate.PairSemantics.raw8093step0 line 565
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical8093 line 567
  117. def OAI.MUB6.Certificate.PairSemantics.raw8094 line 577
  118. def OAI.MUB6.Certificate.PairSemantics.raw8094step0 line 579
  119. def OAI.MUB6.Certificate.PairSemantics.raw8094step1 line 581
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8094 line 583
  121. def OAI.MUB6.Certificate.PairSemantics.raw8095 line 596
  122. def OAI.MUB6.Certificate.PairSemantics.raw8095step0 line 598
  123. def OAI.MUB6.Certificate.PairSemantics.raw8095step1 line 600
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical8095 line 602