OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical18.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw576 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw576step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical576 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw577 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw577step0 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw577step1 line 32
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical577 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw578 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw578step0 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw578step1 line 51
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical578 line 53
  12. def OAI.MUB6.Certificate.PairSemantics.raw579 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw579step0 line 68
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical579 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw580 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw580step0 line 81
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical580 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw581 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw581step0 line 94
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical581 line 96
  21. def OAI.MUB6.Certificate.PairSemantics.raw582 line 105
  22. def OAI.MUB6.Certificate.PairSemantics.raw582step0 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw582step1 line 109
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical582 line 111
  25. def OAI.MUB6.Certificate.PairSemantics.raw583 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw583step0 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw583step1 line 128
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical583 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw584 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw584step0 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw584step1 line 147
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical584 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw585 line 162
  34. def OAI.MUB6.Certificate.PairSemantics.raw585step0 line 164
  35. def OAI.MUB6.Certificate.PairSemantics.raw585step1 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw585step2 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical585 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw586 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw586step0 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw586step1 line 191
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical586 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw587 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw587step0 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw587step1 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical587 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw588 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw588step0 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw588step1 line 229
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical588 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw589 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw589step0 line 246
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical589 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw590 line 257
  54. def OAI.MUB6.Certificate.PairSemantics.raw590step0 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw590step1 line 261
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical590 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw591 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw591step0 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw591step1 line 280
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical591 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw592 line 295
  62. def OAI.MUB6.Certificate.PairSemantics.raw592step0 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw592step1 line 299
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical592 line 301
  65. def OAI.MUB6.Certificate.PairSemantics.raw593 line 314
  66. def OAI.MUB6.Certificate.PairSemantics.raw593step0 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw593step1 line 318
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical593 line 320
  69. def OAI.MUB6.Certificate.PairSemantics.raw594 line 333
  70. def OAI.MUB6.Certificate.PairSemantics.raw594step0 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw594step1 line 337
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical594 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw595 line 352
  74. def OAI.MUB6.Certificate.PairSemantics.raw595step0 line 354
  75. def OAI.MUB6.Certificate.PairSemantics.raw595step1 line 356
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical595 line 358
  77. def OAI.MUB6.Certificate.PairSemantics.raw596 line 371
  78. def OAI.MUB6.Certificate.PairSemantics.raw596step0 line 373
  79. def OAI.MUB6.Certificate.PairSemantics.raw596step1 line 375
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical596 line 377
  81. def OAI.MUB6.Certificate.PairSemantics.raw597 line 390
  82. def OAI.MUB6.Certificate.PairSemantics.raw597step0 line 392
  83. def OAI.MUB6.Certificate.PairSemantics.raw597step1 line 394
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical597 line 396
  85. def OAI.MUB6.Certificate.PairSemantics.raw598 line 409
  86. def OAI.MUB6.Certificate.PairSemantics.raw598step0 line 411
  87. def OAI.MUB6.Certificate.PairSemantics.raw598step1 line 413
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical598 line 415
  89. def OAI.MUB6.Certificate.PairSemantics.raw599 line 428
  90. def OAI.MUB6.Certificate.PairSemantics.raw599step0 line 430
  91. def OAI.MUB6.Certificate.PairSemantics.raw599step1 line 432
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical599 line 434
  93. def OAI.MUB6.Certificate.PairSemantics.raw600 line 447
  94. def OAI.MUB6.Certificate.PairSemantics.raw600step0 line 449
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical600 line 451
  96. def OAI.MUB6.Certificate.PairSemantics.raw601 line 460
  97. def OAI.MUB6.Certificate.PairSemantics.raw601step0 line 462
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical601 line 464
  99. def OAI.MUB6.Certificate.PairSemantics.raw602 line 473
  100. def OAI.MUB6.Certificate.PairSemantics.raw602step0 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw602step1 line 477
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical602 line 479
  103. def OAI.MUB6.Certificate.PairSemantics.raw603 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw603step0 line 494
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical603 line 496
  106. def OAI.MUB6.Certificate.PairSemantics.raw604 line 505
  107. def OAI.MUB6.Certificate.PairSemantics.raw604step0 line 507
  108. def OAI.MUB6.Certificate.PairSemantics.raw604step1 line 509
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical604 line 511
  110. def OAI.MUB6.Certificate.PairSemantics.raw605 line 524
  111. def OAI.MUB6.Certificate.PairSemantics.raw605step0 line 526
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical605 line 528
  113. def OAI.MUB6.Certificate.PairSemantics.raw606 line 537
  114. def OAI.MUB6.Certificate.PairSemantics.raw606step0 line 539
  115. def OAI.MUB6.Certificate.PairSemantics.raw606step1 line 541
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical606 line 543
  117. def OAI.MUB6.Certificate.PairSemantics.raw607 line 556
  118. def OAI.MUB6.Certificate.PairSemantics.raw607step0 line 558
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical607 line 560