OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical107.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3424 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw3424step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw3424step1 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw3424step2 line 28
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical3424 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw3425 line 47
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3425 line 49
  8. def OAI.MUB6.Certificate.PairSemantics.raw3426 line 53
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3426 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw3427 line 59
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3427 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw3428 line 65
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3428 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw3429 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw3429step0 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw3429step1 line 75
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3429 line 77
  18. def OAI.MUB6.Certificate.PairSemantics.raw3430 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw3430step0 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw3430step1 line 94
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3430 line 96
  22. def OAI.MUB6.Certificate.PairSemantics.raw3431 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw3431step0 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw3431step1 line 113
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3431 line 115
  26. def OAI.MUB6.Certificate.PairSemantics.raw3432 line 128
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3432 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw3433 line 134
  29. def OAI.MUB6.Certificate.PairSemantics.raw3433step0 line 136
  30. def OAI.MUB6.Certificate.PairSemantics.raw3433step1 line 138
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3433 line 140
  32. def OAI.MUB6.Certificate.PairSemantics.raw3434 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw3434step0 line 155
  34. def OAI.MUB6.Certificate.PairSemantics.raw3434step1 line 157
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3434 line 159
  36. def OAI.MUB6.Certificate.PairSemantics.raw3435 line 172
  37. def OAI.MUB6.Certificate.PairSemantics.raw3435step0 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw3435step1 line 176
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3435 line 178
  40. def OAI.MUB6.Certificate.PairSemantics.raw3436 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw3436step0 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw3436step1 line 195
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3436 line 197
  44. def OAI.MUB6.Certificate.PairSemantics.raw3437 line 210
  45. def OAI.MUB6.Certificate.PairSemantics.raw3437step0 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw3437step1 line 214
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3437 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw3438 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw3438step0 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw3438step1 line 233
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3438 line 235
  52. def OAI.MUB6.Certificate.PairSemantics.raw3439 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw3439step0 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw3439step1 line 252
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3439 line 254
  56. def OAI.MUB6.Certificate.PairSemantics.raw3440 line 267
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3440 line 269
  58. def OAI.MUB6.Certificate.PairSemantics.raw3441 line 273
  59. def OAI.MUB6.Certificate.PairSemantics.raw3441step0 line 275
  60. def OAI.MUB6.Certificate.PairSemantics.raw3441step1 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw3441step2 line 279
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3441 line 281
  63. def OAI.MUB6.Certificate.PairSemantics.raw3442 line 298
  64. def OAI.MUB6.Certificate.PairSemantics.raw3442step0 line 300
  65. def OAI.MUB6.Certificate.PairSemantics.raw3442step1 line 302
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3442 line 304
  67. def OAI.MUB6.Certificate.PairSemantics.raw3443 line 317
  68. def OAI.MUB6.Certificate.PairSemantics.raw3443step0 line 319
  69. def OAI.MUB6.Certificate.PairSemantics.raw3443step1 line 321
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3443 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw3444 line 336
  72. def OAI.MUB6.Certificate.PairSemantics.raw3444step0 line 338
  73. def OAI.MUB6.Certificate.PairSemantics.raw3444step1 line 340
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical3444 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw3445 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw3445step0 line 357
  77. def OAI.MUB6.Certificate.PairSemantics.raw3445step1 line 359
  78. def OAI.MUB6.Certificate.PairSemantics.raw3445step2 line 361
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3445 line 363
  80. def OAI.MUB6.Certificate.PairSemantics.raw3446 line 380
  81. def OAI.MUB6.Certificate.PairSemantics.raw3446step0 line 382
  82. def OAI.MUB6.Certificate.PairSemantics.raw3446step1 line 384
  83. def OAI.MUB6.Certificate.PairSemantics.raw3446step2 line 386
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3446 line 388
  85. def OAI.MUB6.Certificate.PairSemantics.raw3447 line 405
  86. def OAI.MUB6.Certificate.PairSemantics.raw3447step0 line 407
  87. def OAI.MUB6.Certificate.PairSemantics.raw3447step1 line 409
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical3447 line 411
  89. def OAI.MUB6.Certificate.PairSemantics.raw3448 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw3448step0 line 426
  91. def OAI.MUB6.Certificate.PairSemantics.raw3448step1 line 428
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3448 line 430
  93. def OAI.MUB6.Certificate.PairSemantics.raw3449 line 443
  94. def OAI.MUB6.Certificate.PairSemantics.raw3449step0 line 445
  95. def OAI.MUB6.Certificate.PairSemantics.raw3449step1 line 447
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3449 line 449
  97. def OAI.MUB6.Certificate.PairSemantics.raw3450 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw3450step0 line 464
  99. def OAI.MUB6.Certificate.PairSemantics.raw3450step1 line 466
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3450 line 468
  101. def OAI.MUB6.Certificate.PairSemantics.raw3451 line 481
  102. def OAI.MUB6.Certificate.PairSemantics.raw3451step0 line 483
  103. def OAI.MUB6.Certificate.PairSemantics.raw3451step1 line 485
  104. def OAI.MUB6.Certificate.PairSemantics.raw3451step2 line 487
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3451 line 489
  106. def OAI.MUB6.Certificate.PairSemantics.raw3452 line 506
  107. def OAI.MUB6.Certificate.PairSemantics.raw3452step0 line 508
  108. def OAI.MUB6.Certificate.PairSemantics.raw3452step1 line 510
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3452 line 512
  110. def OAI.MUB6.Certificate.PairSemantics.raw3453 line 525
  111. def OAI.MUB6.Certificate.PairSemantics.raw3453step0 line 527
  112. def OAI.MUB6.Certificate.PairSemantics.raw3453step1 line 529
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical3453 line 531
  114. def OAI.MUB6.Certificate.PairSemantics.raw3454 line 544
  115. def OAI.MUB6.Certificate.PairSemantics.raw3454step0 line 546
  116. def OAI.MUB6.Certificate.PairSemantics.raw3454step1 line 548
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical3454 line 550
  118. def OAI.MUB6.Certificate.PairSemantics.raw3455 line 563
  119. def OAI.MUB6.Certificate.PairSemantics.raw3455step0 line 565
  120. def OAI.MUB6.Certificate.PairSemantics.raw3455step1 line 567
  121. def OAI.MUB6.Certificate.PairSemantics.raw3455step2 line 569
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical3455 line 571