OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical110.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3520 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw3520step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw3520step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3520 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw3521 line 36
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical3521 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw3522 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3522 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw3523 line 48
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical3523 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw3524 line 54
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3524 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw3525 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw3525step0 line 62
  15. def OAI.MUB6.Certificate.PairSemantics.raw3525step1 line 64
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3525 line 66
  17. def OAI.MUB6.Certificate.PairSemantics.raw3526 line 79
  18. def OAI.MUB6.Certificate.PairSemantics.raw3526step0 line 81
  19. def OAI.MUB6.Certificate.PairSemantics.raw3526step1 line 83
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3526 line 85
  21. def OAI.MUB6.Certificate.PairSemantics.raw3527 line 98
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3527 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw3528 line 104
  24. def OAI.MUB6.Certificate.PairSemantics.raw3528step0 line 106
  25. def OAI.MUB6.Certificate.PairSemantics.raw3528step1 line 108
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3528 line 110
  27. def OAI.MUB6.Certificate.PairSemantics.raw3529 line 123
  28. def OAI.MUB6.Certificate.PairSemantics.raw3529step0 line 125
  29. def OAI.MUB6.Certificate.PairSemantics.raw3529step1 line 127
  30. def OAI.MUB6.Certificate.PairSemantics.raw3529step2 line 129
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3529 line 131
  32. def OAI.MUB6.Certificate.PairSemantics.raw3530 line 148
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3530 line 150
  34. def OAI.MUB6.Certificate.PairSemantics.raw3531 line 154
  35. def OAI.MUB6.Certificate.PairSemantics.raw3531step0 line 156
  36. def OAI.MUB6.Certificate.PairSemantics.raw3531step1 line 158
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3531 line 160
  38. def OAI.MUB6.Certificate.PairSemantics.raw3532 line 173
  39. def OAI.MUB6.Certificate.PairSemantics.raw3532step0 line 175
  40. def OAI.MUB6.Certificate.PairSemantics.raw3532step1 line 177
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3532 line 179
  42. def OAI.MUB6.Certificate.PairSemantics.raw3533 line 192
  43. def OAI.MUB6.Certificate.PairSemantics.raw3533step0 line 194
  44. def OAI.MUB6.Certificate.PairSemantics.raw3533step1 line 196
  45. def OAI.MUB6.Certificate.PairSemantics.raw3533step2 line 198
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3533 line 200
  47. def OAI.MUB6.Certificate.PairSemantics.raw3534 line 217
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3534 line 219
  49. def OAI.MUB6.Certificate.PairSemantics.raw3535 line 223
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3535 line 225
  51. def OAI.MUB6.Certificate.PairSemantics.raw3536 line 229
  52. def OAI.MUB6.Certificate.PairSemantics.raw3536step0 line 231
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3536 line 233
  54. def OAI.MUB6.Certificate.PairSemantics.raw3537 line 242
  55. def OAI.MUB6.Certificate.PairSemantics.raw3537step0 line 244
  56. def OAI.MUB6.Certificate.PairSemantics.raw3537step1 line 246
  57. def OAI.MUB6.Certificate.PairSemantics.raw3537step2 line 248
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical3537 line 250
  59. def OAI.MUB6.Certificate.PairSemantics.raw3538 line 267
  60. def OAI.MUB6.Certificate.PairSemantics.raw3538step0 line 269
  61. def OAI.MUB6.Certificate.PairSemantics.raw3538step1 line 271
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3538 line 273
  63. def OAI.MUB6.Certificate.PairSemantics.raw3539 line 286
  64. def OAI.MUB6.Certificate.PairSemantics.raw3539step0 line 288
  65. def OAI.MUB6.Certificate.PairSemantics.raw3539step1 line 290
  66. def OAI.MUB6.Certificate.PairSemantics.raw3539step2 line 292
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical3539 line 294
  68. def OAI.MUB6.Certificate.PairSemantics.raw3540 line 311
  69. def OAI.MUB6.Certificate.PairSemantics.raw3540step0 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw3540step1 line 315
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical3540 line 317
  72. def OAI.MUB6.Certificate.PairSemantics.raw3541 line 330
  73. def OAI.MUB6.Certificate.PairSemantics.raw3541step0 line 332
  74. def OAI.MUB6.Certificate.PairSemantics.raw3541step1 line 334
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3541 line 336
  76. def OAI.MUB6.Certificate.PairSemantics.raw3542 line 349
  77. def OAI.MUB6.Certificate.PairSemantics.raw3542step0 line 351
  78. def OAI.MUB6.Certificate.PairSemantics.raw3542step1 line 353
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3542 line 355
  80. def OAI.MUB6.Certificate.PairSemantics.raw3543 line 368
  81. def OAI.MUB6.Certificate.PairSemantics.raw3543step0 line 370
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3543 line 372
  83. def OAI.MUB6.Certificate.PairSemantics.raw3544 line 381
  84. def OAI.MUB6.Certificate.PairSemantics.raw3544step0 line 383
  85. def OAI.MUB6.Certificate.PairSemantics.raw3544step1 line 385
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3544 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw3545 line 400
  88. def OAI.MUB6.Certificate.PairSemantics.raw3545step0 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw3545step1 line 404
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3545 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw3546 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw3546step0 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw3546step1 line 423
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3546 line 425
  95. def OAI.MUB6.Certificate.PairSemantics.raw3547 line 438
  96. def OAI.MUB6.Certificate.PairSemantics.raw3547step0 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw3547step1 line 442
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3547 line 444
  99. def OAI.MUB6.Certificate.PairSemantics.raw3548 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw3548step0 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw3548step1 line 461
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3548 line 463
  103. def OAI.MUB6.Certificate.PairSemantics.raw3549 line 476
  104. def OAI.MUB6.Certificate.PairSemantics.raw3549step0 line 478
  105. def OAI.MUB6.Certificate.PairSemantics.raw3549step1 line 480
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical3549 line 482
  107. def OAI.MUB6.Certificate.PairSemantics.raw3550 line 495
  108. def OAI.MUB6.Certificate.PairSemantics.raw3550step0 line 497
  109. def OAI.MUB6.Certificate.PairSemantics.raw3550step1 line 499
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical3550 line 501
  111. def OAI.MUB6.Certificate.PairSemantics.raw3551 line 514
  112. def OAI.MUB6.Certificate.PairSemantics.raw3551step0 line 516
  113. def OAI.MUB6.Certificate.PairSemantics.raw3551step1 line 518
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical3551 line 520