OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical294.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9408 line 24
  2. def OAI.MUB6.Certificate.PairSemantics.raw9408step0 line 26
  3. def OAI.MUB6.Certificate.PairSemantics.raw9408step1 line 28
  4. def OAI.MUB6.Certificate.PairSemantics.raw9408step2 line 30
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical9408 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw9409 line 50
  7. def OAI.MUB6.Certificate.PairSemantics.raw9409step0 line 52
  8. def OAI.MUB6.Certificate.PairSemantics.raw9409step1 line 54
  9. def OAI.MUB6.Certificate.PairSemantics.raw9409step2 line 56
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9409 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw9410 line 76
  12. def OAI.MUB6.Certificate.PairSemantics.raw9410step0 line 78
  13. def OAI.MUB6.Certificate.PairSemantics.raw9410step1 line 80
  14. def OAI.MUB6.Certificate.PairSemantics.raw9410step2 line 82
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9410 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw9411 line 102
  17. def OAI.MUB6.Certificate.PairSemantics.raw9411step0 line 104
  18. def OAI.MUB6.Certificate.PairSemantics.raw9411step1 line 106
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9411 line 108
  20. def OAI.MUB6.Certificate.PairSemantics.raw9412 line 122
  21. def OAI.MUB6.Certificate.PairSemantics.raw9412step0 line 124
  22. def OAI.MUB6.Certificate.PairSemantics.raw9412step1 line 126
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9412 line 128
  24. def OAI.MUB6.Certificate.PairSemantics.raw9413 line 142
  25. def OAI.MUB6.Certificate.PairSemantics.raw9413step0 line 144
  26. def OAI.MUB6.Certificate.PairSemantics.raw9413step1 line 146
  27. def OAI.MUB6.Certificate.PairSemantics.raw9413step2 line 148
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9413 line 150
  29. def OAI.MUB6.Certificate.PairSemantics.raw9414 line 168
  30. def OAI.MUB6.Certificate.PairSemantics.raw9414step0 line 170
  31. def OAI.MUB6.Certificate.PairSemantics.raw9414step1 line 172
  32. def OAI.MUB6.Certificate.PairSemantics.raw9414step2 line 174
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9414 line 176
  34. def OAI.MUB6.Certificate.PairSemantics.raw9415 line 194
  35. def OAI.MUB6.Certificate.PairSemantics.raw9415step0 line 196
  36. def OAI.MUB6.Certificate.PairSemantics.raw9415step1 line 198
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9415 line 200
  38. def OAI.MUB6.Certificate.PairSemantics.raw9416 line 214
  39. def OAI.MUB6.Certificate.PairSemantics.raw9416step0 line 216
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9416 line 218
  41. def OAI.MUB6.Certificate.PairSemantics.raw9417 line 227
  42. def OAI.MUB6.Certificate.PairSemantics.raw9417step0 line 229
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9417 line 231
  44. def OAI.MUB6.Certificate.PairSemantics.raw9418 line 240
  45. def OAI.MUB6.Certificate.PairSemantics.raw9418step0 line 242
  46. def OAI.MUB6.Certificate.PairSemantics.raw9418step1 line 244
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9418 line 246
  48. def OAI.MUB6.Certificate.PairSemantics.raw9419 line 259
  49. def OAI.MUB6.Certificate.PairSemantics.raw9419step0 line 261
  50. def OAI.MUB6.Certificate.PairSemantics.raw9419step1 line 263
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical9419 line 265
  52. def OAI.MUB6.Certificate.PairSemantics.raw9420 line 278
  53. def OAI.MUB6.Certificate.PairSemantics.raw9420step0 line 280
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9420 line 282
  55. def OAI.MUB6.Certificate.PairSemantics.raw9421 line 291
  56. def OAI.MUB6.Certificate.PairSemantics.raw9421step0 line 293
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9421 line 295
  58. def OAI.MUB6.Certificate.PairSemantics.raw9422 line 304
  59. def OAI.MUB6.Certificate.PairSemantics.raw9422step0 line 306
  60. def OAI.MUB6.Certificate.PairSemantics.raw9422step1 line 308
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9422 line 310
  62. def OAI.MUB6.Certificate.PairSemantics.raw9423 line 323
  63. def OAI.MUB6.Certificate.PairSemantics.raw9423step0 line 325
  64. def OAI.MUB6.Certificate.PairSemantics.raw9423step1 line 327
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9423 line 329
  66. def OAI.MUB6.Certificate.PairSemantics.raw9424 line 343
  67. def OAI.MUB6.Certificate.PairSemantics.raw9424step0 line 345
  68. def OAI.MUB6.Certificate.PairSemantics.raw9424step1 line 347
  69. def OAI.MUB6.Certificate.PairSemantics.raw9424step2 line 349
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9424 line 351
  71. def OAI.MUB6.Certificate.PairSemantics.raw9425 line 369
  72. def OAI.MUB6.Certificate.PairSemantics.raw9425step0 line 371
  73. def OAI.MUB6.Certificate.PairSemantics.raw9425step1 line 373
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9425 line 375
  75. def OAI.MUB6.Certificate.PairSemantics.raw9426 line 389
  76. def OAI.MUB6.Certificate.PairSemantics.raw9426step0 line 391
  77. def OAI.MUB6.Certificate.PairSemantics.raw9426step1 line 393
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9426 line 395
  79. def OAI.MUB6.Certificate.PairSemantics.raw9427 line 409
  80. def OAI.MUB6.Certificate.PairSemantics.raw9427step0 line 411
  81. def OAI.MUB6.Certificate.PairSemantics.raw9427step1 line 413
  82. def OAI.MUB6.Certificate.PairSemantics.raw9427step2 line 415
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9427 line 417
  84. def OAI.MUB6.Certificate.PairSemantics.raw9428 line 435
  85. def OAI.MUB6.Certificate.PairSemantics.raw9428step0 line 437
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9428 line 439
  87. def OAI.MUB6.Certificate.PairSemantics.raw9429 line 448
  88. def OAI.MUB6.Certificate.PairSemantics.raw9429step0 line 450
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9429 line 452
  90. def OAI.MUB6.Certificate.PairSemantics.raw9430 line 461
  91. def OAI.MUB6.Certificate.PairSemantics.raw9430step0 line 463
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9430 line 465
  93. def OAI.MUB6.Certificate.PairSemantics.raw9431 line 474
  94. def OAI.MUB6.Certificate.PairSemantics.raw9431step0 line 476
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9431 line 478
  96. def OAI.MUB6.Certificate.PairSemantics.raw9432 line 487
  97. def OAI.MUB6.Certificate.PairSemantics.raw9432step0 line 489
  98. def OAI.MUB6.Certificate.PairSemantics.raw9432step1 line 491
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9432 line 493
  100. def OAI.MUB6.Certificate.PairSemantics.raw9433 line 506
  101. def OAI.MUB6.Certificate.PairSemantics.raw9433step0 line 508
  102. def OAI.MUB6.Certificate.PairSemantics.raw9433step1 line 510
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9433 line 512
  104. def OAI.MUB6.Certificate.PairSemantics.raw9434 line 525
  105. def OAI.MUB6.Certificate.PairSemantics.raw9434step0 line 527
  106. def OAI.MUB6.Certificate.PairSemantics.raw9434step1 line 529
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9434 line 531
  108. def OAI.MUB6.Certificate.PairSemantics.raw9435 line 545
  109. def OAI.MUB6.Certificate.PairSemantics.raw9435step0 line 547
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical9435 line 549
  111. def OAI.MUB6.Certificate.PairSemantics.raw9436 line 558
  112. def OAI.MUB6.Certificate.PairSemantics.raw9436step0 line 560
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical9436 line 562
  114. def OAI.MUB6.Certificate.PairSemantics.raw9437 line 571
  115. def OAI.MUB6.Certificate.PairSemantics.raw9437step0 line 573
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical9437 line 575
  117. def OAI.MUB6.Certificate.PairSemantics.raw9438 line 584
  118. def OAI.MUB6.Certificate.PairSemantics.raw9438step0 line 586
  119. def OAI.MUB6.Certificate.PairSemantics.raw9438step1 line 588
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical9438 line 590
  121. def OAI.MUB6.Certificate.PairSemantics.raw9439 line 603
  122. def OAI.MUB6.Certificate.PairSemantics.raw9439step0 line 605
  123. def OAI.MUB6.Certificate.PairSemantics.raw9439step1 line 607
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical9439 line 609