OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical263.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8416 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8416step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw8416step1 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8416step2 line 25
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8416 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw8417 line 45
  7. def OAI.MUB6.Certificate.PairSemantics.raw8417step0 line 47
  8. def OAI.MUB6.Certificate.PairSemantics.raw8417step1 line 49
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8417 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw8418 line 65
  11. def OAI.MUB6.Certificate.PairSemantics.raw8418step0 line 67
  12. def OAI.MUB6.Certificate.PairSemantics.raw8418step1 line 69
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8418 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw8419 line 84
  15. def OAI.MUB6.Certificate.PairSemantics.raw8419step0 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw8419step1 line 88
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8419 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw8420 line 103
  19. def OAI.MUB6.Certificate.PairSemantics.raw8420step0 line 105
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8420 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw8421 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw8421step0 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw8421step1 line 120
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8421 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw8422 line 135
  26. def OAI.MUB6.Certificate.PairSemantics.raw8422step0 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw8422step1 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw8422step2 line 141
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8422 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw8423 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw8423step0 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw8423step1 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw8423step2 line 166
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8423 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw8424 line 185
  36. def OAI.MUB6.Certificate.PairSemantics.raw8424step0 line 187
  37. def OAI.MUB6.Certificate.PairSemantics.raw8424step1 line 189
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8424 line 191
  39. def OAI.MUB6.Certificate.PairSemantics.raw8425 line 204
  40. def OAI.MUB6.Certificate.PairSemantics.raw8425step0 line 206
  41. def OAI.MUB6.Certificate.PairSemantics.raw8425step1 line 208
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8425 line 210
  43. def OAI.MUB6.Certificate.PairSemantics.raw8426 line 223
  44. def OAI.MUB6.Certificate.PairSemantics.raw8426step0 line 225
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8426 line 227
  46. def OAI.MUB6.Certificate.PairSemantics.raw8427 line 236
  47. def OAI.MUB6.Certificate.PairSemantics.raw8427step0 line 238
  48. def OAI.MUB6.Certificate.PairSemantics.raw8427step1 line 240
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8427 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw8428 line 255
  51. def OAI.MUB6.Certificate.PairSemantics.raw8428step0 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw8428step1 line 259
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8428 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw8429 line 274
  55. def OAI.MUB6.Certificate.PairSemantics.raw8429step0 line 276
  56. def OAI.MUB6.Certificate.PairSemantics.raw8429step1 line 278
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8429 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw8430 line 293
  59. def OAI.MUB6.Certificate.PairSemantics.raw8430step0 line 295
  60. def OAI.MUB6.Certificate.PairSemantics.raw8430step1 line 297
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8430 line 299
  62. def OAI.MUB6.Certificate.PairSemantics.raw8431 line 312
  63. def OAI.MUB6.Certificate.PairSemantics.raw8431step0 line 314
  64. def OAI.MUB6.Certificate.PairSemantics.raw8431step1 line 316
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8431 line 318
  66. def OAI.MUB6.Certificate.PairSemantics.raw8432 line 331
  67. def OAI.MUB6.Certificate.PairSemantics.raw8432step0 line 333
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8432 line 335
  69. def OAI.MUB6.Certificate.PairSemantics.raw8433 line 344
  70. def OAI.MUB6.Certificate.PairSemantics.raw8433step0 line 346
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8433 line 348
  72. def OAI.MUB6.Certificate.PairSemantics.raw8434 line 357
  73. def OAI.MUB6.Certificate.PairSemantics.raw8434step0 line 359
  74. def OAI.MUB6.Certificate.PairSemantics.raw8434step1 line 361
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8434 line 363
  76. def OAI.MUB6.Certificate.PairSemantics.raw8435 line 376
  77. def OAI.MUB6.Certificate.PairSemantics.raw8435step0 line 378
  78. def OAI.MUB6.Certificate.PairSemantics.raw8435step1 line 380
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8435 line 382
  80. def OAI.MUB6.Certificate.PairSemantics.raw8436 line 395
  81. def OAI.MUB6.Certificate.PairSemantics.raw8436step0 line 397
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8436 line 399
  83. def OAI.MUB6.Certificate.PairSemantics.raw8437 line 408
  84. def OAI.MUB6.Certificate.PairSemantics.raw8437step0 line 410
  85. def OAI.MUB6.Certificate.PairSemantics.raw8437step1 line 412
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8437 line 414
  87. def OAI.MUB6.Certificate.PairSemantics.raw8438 line 427
  88. def OAI.MUB6.Certificate.PairSemantics.raw8438step0 line 429
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8438 line 431
  90. def OAI.MUB6.Certificate.PairSemantics.raw8439 line 440
  91. def OAI.MUB6.Certificate.PairSemantics.raw8439step0 line 442
  92. def OAI.MUB6.Certificate.PairSemantics.raw8439step1 line 444
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8439 line 446
  94. def OAI.MUB6.Certificate.PairSemantics.raw8440 line 459
  95. def OAI.MUB6.Certificate.PairSemantics.raw8440step0 line 461
  96. def OAI.MUB6.Certificate.PairSemantics.raw8440step1 line 463
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical8440 line 465
  98. def OAI.MUB6.Certificate.PairSemantics.raw8441 line 478
  99. def OAI.MUB6.Certificate.PairSemantics.raw8441step0 line 480
  100. def OAI.MUB6.Certificate.PairSemantics.raw8441step1 line 482
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8441 line 484
  102. def OAI.MUB6.Certificate.PairSemantics.raw8442 line 497
  103. def OAI.MUB6.Certificate.PairSemantics.raw8442step0 line 499
  104. def OAI.MUB6.Certificate.PairSemantics.raw8442step1 line 501
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical8442 line 503
  106. def OAI.MUB6.Certificate.PairSemantics.raw8443 line 516
  107. def OAI.MUB6.Certificate.PairSemantics.raw8443step0 line 518
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical8443 line 520
  109. def OAI.MUB6.Certificate.PairSemantics.raw8444 line 529
  110. def OAI.MUB6.Certificate.PairSemantics.raw8444step0 line 531
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8444 line 533
  112. def OAI.MUB6.Certificate.PairSemantics.raw8445 line 542
  113. def OAI.MUB6.Certificate.PairSemantics.raw8445step0 line 544
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8445 line 546
  115. def OAI.MUB6.Certificate.PairSemantics.raw8446 line 555
  116. def OAI.MUB6.Certificate.PairSemantics.raw8446step0 line 557
  117. def OAI.MUB6.Certificate.PairSemantics.raw8446step1 line 559
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical8446 line 561
  119. def OAI.MUB6.Certificate.PairSemantics.raw8447 line 574
  120. def OAI.MUB6.Certificate.PairSemantics.raw8447step0 line 576
  121. def OAI.MUB6.Certificate.PairSemantics.raw8447step1 line 578
  122. def OAI.MUB6.Certificate.PairSemantics.raw8447step2 line 580
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical8447 line 582