OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical268.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8576 line 24
  2. def OAI.MUB6.Certificate.PairSemantics.raw8576step0 line 26
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8576 line 28
  4. def OAI.MUB6.Certificate.PairSemantics.raw8577 line 37
  5. def OAI.MUB6.Certificate.PairSemantics.raw8577step0 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw8577step1 line 41
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8577 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw8578 line 56
  9. def OAI.MUB6.Certificate.PairSemantics.raw8578step0 line 58
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8578 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw8579 line 69
  12. def OAI.MUB6.Certificate.PairSemantics.raw8579step0 line 71
  13. def OAI.MUB6.Certificate.PairSemantics.raw8579step1 line 73
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8579 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw8580 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw8580step0 line 90
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8580 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw8581 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw8581step0 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw8581step1 line 105
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8581 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw8582 line 120
  23. def OAI.MUB6.Certificate.PairSemantics.raw8582step0 line 122
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8582 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw8583 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw8583step0 line 135
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8583 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw8584 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw8584step0 line 148
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8584 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw8585 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw8585step0 line 161
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8585 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw8586 line 172
  35. def OAI.MUB6.Certificate.PairSemantics.raw8586step0 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw8586step1 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw8586step2 line 178
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8586 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw8587 line 198
  40. def OAI.MUB6.Certificate.PairSemantics.raw8587step0 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw8587step1 line 202
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8587 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw8588 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw8588step0 line 220
  45. def OAI.MUB6.Certificate.PairSemantics.raw8588step1 line 222
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical8588 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw8589 line 238
  48. def OAI.MUB6.Certificate.PairSemantics.raw8589step0 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw8589step1 line 242
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8589 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw8590 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw8590step0 line 259
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8590 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw8591 line 270
  55. def OAI.MUB6.Certificate.PairSemantics.raw8591step0 line 272
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8591 line 274
  57. def OAI.MUB6.Certificate.PairSemantics.raw8592 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw8592step0 line 286
  59. def OAI.MUB6.Certificate.PairSemantics.raw8592step1 line 288
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8592 line 290
  61. def OAI.MUB6.Certificate.PairSemantics.raw8593 line 304
  62. def OAI.MUB6.Certificate.PairSemantics.raw8593step0 line 306
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical8593 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw8594 line 317
  65. def OAI.MUB6.Certificate.PairSemantics.raw8594step0 line 319
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8594 line 321
  67. def OAI.MUB6.Certificate.PairSemantics.raw8595 line 330
  68. def OAI.MUB6.Certificate.PairSemantics.raw8595step0 line 332
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8595 line 334
  70. def OAI.MUB6.Certificate.PairSemantics.raw8596 line 343
  71. def OAI.MUB6.Certificate.PairSemantics.raw8596step0 line 345
  72. def OAI.MUB6.Certificate.PairSemantics.raw8596step1 line 347
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8596 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw8597 line 363
  75. def OAI.MUB6.Certificate.PairSemantics.raw8597step0 line 365
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8597 line 367
  77. def OAI.MUB6.Certificate.PairSemantics.raw8598 line 376
  78. def OAI.MUB6.Certificate.PairSemantics.raw8598step0 line 378
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8598 line 380
  80. def OAI.MUB6.Certificate.PairSemantics.raw8599 line 389
  81. def OAI.MUB6.Certificate.PairSemantics.raw8599step0 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw8599step1 line 393
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8599 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw8600 line 409
  85. def OAI.MUB6.Certificate.PairSemantics.raw8600step0 line 411
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8600 line 413
  87. def OAI.MUB6.Certificate.PairSemantics.raw8601 line 422
  88. def OAI.MUB6.Certificate.PairSemantics.raw8601step0 line 424
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8601 line 426
  90. def OAI.MUB6.Certificate.PairSemantics.raw8602 line 435
  91. def OAI.MUB6.Certificate.PairSemantics.raw8602step0 line 437
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical8602 line 439
  93. def OAI.MUB6.Certificate.PairSemantics.raw8603 line 448
  94. def OAI.MUB6.Certificate.PairSemantics.raw8603step0 line 450
  95. def OAI.MUB6.Certificate.PairSemantics.raw8603step1 line 452
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8603 line 454
  97. def OAI.MUB6.Certificate.PairSemantics.raw8604 line 468
  98. def OAI.MUB6.Certificate.PairSemantics.raw8604step0 line 470
  99. def OAI.MUB6.Certificate.PairSemantics.raw8604step1 line 472
  100. def OAI.MUB6.Certificate.PairSemantics.raw8604step2 line 474
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8604 line 476
  102. def OAI.MUB6.Certificate.PairSemantics.raw8605 line 494
  103. def OAI.MUB6.Certificate.PairSemantics.raw8605step0 line 496
  104. def OAI.MUB6.Certificate.PairSemantics.raw8605step1 line 498
  105. def OAI.MUB6.Certificate.PairSemantics.raw8605step2 line 500
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8605 line 502
  107. def OAI.MUB6.Certificate.PairSemantics.raw8606 line 520
  108. def OAI.MUB6.Certificate.PairSemantics.raw8606step0 line 522
  109. def OAI.MUB6.Certificate.PairSemantics.raw8606step1 line 524
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8606 line 526
  111. def OAI.MUB6.Certificate.PairSemantics.raw8607 line 541
  112. def OAI.MUB6.Certificate.PairSemantics.raw8607step0 line 543
  113. def OAI.MUB6.Certificate.PairSemantics.raw8607step1 line 545
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8607 line 547