OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical274.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8768 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw8768step0 line 23
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8768 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw8769 line 34
  5. def OAI.MUB6.Certificate.PairSemantics.raw8769step0 line 36
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8769 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw8770 line 47
  8. def OAI.MUB6.Certificate.PairSemantics.raw8770step0 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw8770step1 line 51
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8770 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw8771 line 67
  12. def OAI.MUB6.Certificate.PairSemantics.raw8771step0 line 69
  13. def OAI.MUB6.Certificate.PairSemantics.raw8771step1 line 71
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8771 line 73
  15. def OAI.MUB6.Certificate.PairSemantics.raw8772 line 87
  16. def OAI.MUB6.Certificate.PairSemantics.raw8772step0 line 89
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8772 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw8773 line 100
  19. def OAI.MUB6.Certificate.PairSemantics.raw8773step0 line 102
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8773 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw8774 line 113
  22. def OAI.MUB6.Certificate.PairSemantics.raw8774step0 line 115
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8774 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw8775 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw8775step0 line 128
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical8775 line 130
  27. def OAI.MUB6.Certificate.PairSemantics.raw8776 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw8776step0 line 141
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8776 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw8777 line 152
  31. def OAI.MUB6.Certificate.PairSemantics.raw8777step0 line 154
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8777 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw8778 line 165
  34. def OAI.MUB6.Certificate.PairSemantics.raw8778step0 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw8778step1 line 169
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical8778 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw8779 line 185
  38. def OAI.MUB6.Certificate.PairSemantics.raw8779step0 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw8779step1 line 189
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8779 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw8780 line 204
  42. def OAI.MUB6.Certificate.PairSemantics.raw8780step0 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw8780step1 line 208
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8780 line 210
  45. def OAI.MUB6.Certificate.PairSemantics.raw8781 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw8781step0 line 225
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8781 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw8782 line 236
  49. def OAI.MUB6.Certificate.PairSemantics.raw8782step0 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw8782step1 line 240
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8782 line 242
  52. def OAI.MUB6.Certificate.PairSemantics.raw8783 line 255
  53. def OAI.MUB6.Certificate.PairSemantics.raw8783step0 line 257
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8783 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw8784 line 268
  56. def OAI.MUB6.Certificate.PairSemantics.raw8784step0 line 270
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8784 line 272
  58. def OAI.MUB6.Certificate.PairSemantics.raw8785 line 281
  59. def OAI.MUB6.Certificate.PairSemantics.raw8785step0 line 283
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8785 line 285
  61. def OAI.MUB6.Certificate.PairSemantics.raw8786 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw8786step0 line 296
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical8786 line 298
  64. def OAI.MUB6.Certificate.PairSemantics.raw8787 line 307
  65. def OAI.MUB6.Certificate.PairSemantics.raw8787step0 line 309
  66. def OAI.MUB6.Certificate.PairSemantics.raw8787step1 line 311
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical8787 line 313
  68. def OAI.MUB6.Certificate.PairSemantics.raw8788 line 326
  69. def OAI.MUB6.Certificate.PairSemantics.raw8788step0 line 328
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8788 line 330
  71. def OAI.MUB6.Certificate.PairSemantics.raw8789 line 339
  72. def OAI.MUB6.Certificate.PairSemantics.raw8789step0 line 341
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8789 line 343
  74. def OAI.MUB6.Certificate.PairSemantics.raw8790 line 352
  75. def OAI.MUB6.Certificate.PairSemantics.raw8790step0 line 354
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8790 line 356
  77. def OAI.MUB6.Certificate.PairSemantics.raw8791 line 365
  78. def OAI.MUB6.Certificate.PairSemantics.raw8791step0 line 367
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8791 line 369
  80. def OAI.MUB6.Certificate.PairSemantics.raw8792 line 378
  81. def OAI.MUB6.Certificate.PairSemantics.raw8792step0 line 380
  82. def OAI.MUB6.Certificate.PairSemantics.raw8792step1 line 382
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8792 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw8793 line 397
  85. def OAI.MUB6.Certificate.PairSemantics.raw8793step0 line 399
  86. def OAI.MUB6.Certificate.PairSemantics.raw8793step1 line 401
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8793 line 403
  88. def OAI.MUB6.Certificate.PairSemantics.raw8794 line 416
  89. def OAI.MUB6.Certificate.PairSemantics.raw8794step0 line 418
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical8794 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw8795 line 429
  92. def OAI.MUB6.Certificate.PairSemantics.raw8795step0 line 431
  93. def OAI.MUB6.Certificate.PairSemantics.raw8795step1 line 433
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8795 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw8796 line 448
  96. def OAI.MUB6.Certificate.PairSemantics.raw8796step0 line 450
  97. def OAI.MUB6.Certificate.PairSemantics.raw8796step1 line 452
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical8796 line 454
  99. def OAI.MUB6.Certificate.PairSemantics.raw8797 line 467
  100. def OAI.MUB6.Certificate.PairSemantics.raw8797step0 line 469
  101. def OAI.MUB6.Certificate.PairSemantics.raw8797step1 line 471
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8797 line 473
  103. def OAI.MUB6.Certificate.PairSemantics.raw8798 line 486
  104. def OAI.MUB6.Certificate.PairSemantics.raw8798step0 line 488
  105. def OAI.MUB6.Certificate.PairSemantics.raw8798step1 line 490
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8798 line 492
  107. def OAI.MUB6.Certificate.PairSemantics.raw8799 line 505
  108. def OAI.MUB6.Certificate.PairSemantics.raw8799step0 line 507
  109. def OAI.MUB6.Certificate.PairSemantics.raw8799step1 line 509
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8799 line 511