OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical19.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw608 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw608step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw608step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical608 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw609 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw609step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw609step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical609 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw610 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw610step0 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw610step1 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical610 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw611 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw611step0 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw611step1 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical611 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw612 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw612step0 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw612step1 line 96
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical612 line 98
  21. def OAI.MUB6.Certificate.PairSemantics.raw613 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw613step0 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw613step1 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical613 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw614 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw614step0 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical614 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw615 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw615step0 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw615step1 line 147
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical615 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw616 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw616step0 line 164
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical616 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw617 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw617step0 line 177
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical617 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw618 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw618step0 line 190
  40. def OAI.MUB6.Certificate.PairSemantics.raw618step1 line 192
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical618 line 194
  42. def OAI.MUB6.Certificate.PairSemantics.raw619 line 207
  43. def OAI.MUB6.Certificate.PairSemantics.raw619step0 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw619step1 line 211
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical619 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw620 line 226
  47. def OAI.MUB6.Certificate.PairSemantics.raw620step0 line 228
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical620 line 230
  49. def OAI.MUB6.Certificate.PairSemantics.raw621 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw621step0 line 241
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical621 line 243
  52. def OAI.MUB6.Certificate.PairSemantics.raw622 line 252
  53. def OAI.MUB6.Certificate.PairSemantics.raw622step0 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw622step1 line 256
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical622 line 258
  56. def OAI.MUB6.Certificate.PairSemantics.raw623 line 271
  57. def OAI.MUB6.Certificate.PairSemantics.raw623step0 line 273
  58. def OAI.MUB6.Certificate.PairSemantics.raw623step1 line 275
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical623 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw624 line 290
  61. def OAI.MUB6.Certificate.PairSemantics.raw624step0 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw624step1 line 294
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical624 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw625 line 309
  65. def OAI.MUB6.Certificate.PairSemantics.raw625step0 line 311
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical625 line 313
  67. def OAI.MUB6.Certificate.PairSemantics.raw626 line 322
  68. def OAI.MUB6.Certificate.PairSemantics.raw626step0 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw626step1 line 326
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical626 line 328
  71. def OAI.MUB6.Certificate.PairSemantics.raw627 line 341
  72. def OAI.MUB6.Certificate.PairSemantics.raw627step0 line 343
  73. def OAI.MUB6.Certificate.PairSemantics.raw627step1 line 345
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical627 line 347
  75. def OAI.MUB6.Certificate.PairSemantics.raw628 line 360
  76. def OAI.MUB6.Certificate.PairSemantics.raw628step0 line 362
  77. def OAI.MUB6.Certificate.PairSemantics.raw628step1 line 364
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical628 line 366
  79. def OAI.MUB6.Certificate.PairSemantics.raw629 line 379
  80. def OAI.MUB6.Certificate.PairSemantics.raw629step0 line 381
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical629 line 383
  82. def OAI.MUB6.Certificate.PairSemantics.raw630 line 392
  83. def OAI.MUB6.Certificate.PairSemantics.raw630step0 line 394
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical630 line 396
  85. def OAI.MUB6.Certificate.PairSemantics.raw631 line 405
  86. def OAI.MUB6.Certificate.PairSemantics.raw631step0 line 407
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical631 line 409
  88. def OAI.MUB6.Certificate.PairSemantics.raw632 line 418
  89. def OAI.MUB6.Certificate.PairSemantics.raw632step0 line 420
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical632 line 422
  91. def OAI.MUB6.Certificate.PairSemantics.raw633 line 431
  92. def OAI.MUB6.Certificate.PairSemantics.raw633step0 line 433
  93. def OAI.MUB6.Certificate.PairSemantics.raw633step1 line 435
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical633 line 437
  95. def OAI.MUB6.Certificate.PairSemantics.raw634 line 450
  96. def OAI.MUB6.Certificate.PairSemantics.raw634step0 line 452
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical634 line 454
  98. def OAI.MUB6.Certificate.PairSemantics.raw635 line 463
  99. def OAI.MUB6.Certificate.PairSemantics.raw635step0 line 465
  100. def OAI.MUB6.Certificate.PairSemantics.raw635step1 line 467
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical635 line 469
  102. def OAI.MUB6.Certificate.PairSemantics.raw636 line 482
  103. def OAI.MUB6.Certificate.PairSemantics.raw636step0 line 484
  104. def OAI.MUB6.Certificate.PairSemantics.raw636step1 line 486
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical636 line 488
  106. def OAI.MUB6.Certificate.PairSemantics.raw637 line 501
  107. def OAI.MUB6.Certificate.PairSemantics.raw637step0 line 503
  108. def OAI.MUB6.Certificate.PairSemantics.raw637step1 line 505
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical637 line 507
  110. def OAI.MUB6.Certificate.PairSemantics.raw638 line 520
  111. def OAI.MUB6.Certificate.PairSemantics.raw638step0 line 522
  112. def OAI.MUB6.Certificate.PairSemantics.raw638step1 line 524
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical638 line 526
  114. def OAI.MUB6.Certificate.PairSemantics.raw639 line 539
  115. def OAI.MUB6.Certificate.PairSemantics.raw639step0 line 541
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical639 line 543