OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical117.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3744 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw3744step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw3744step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3744 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw3745 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw3745step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw3745step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3745 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw3746 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw3746step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw3746step1 line 64
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3746 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw3747 line 79
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3747 line 81
  15. def OAI.MUB6.Certificate.PairSemantics.raw3748 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw3748step0 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw3748step1 line 89
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3748 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw3749 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw3749step0 line 106
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3749 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw3750 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw3750step0 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw3750step1 line 121
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3750 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw3751 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3751 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw3752 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw3752step0 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3752 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw3753 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw3753step0 line 157
  33. def OAI.MUB6.Certificate.PairSemantics.raw3753step1 line 159
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3753 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw3754 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw3754step0 line 176
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3754 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3755 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw3755step0 line 189
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3755 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw3756 line 200
  42. def OAI.MUB6.Certificate.PairSemantics.raw3756step0 line 202
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3756 line 204
  44. def OAI.MUB6.Certificate.PairSemantics.raw3757 line 213
  45. def OAI.MUB6.Certificate.PairSemantics.raw3757step0 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw3757step1 line 217
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3757 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw3758 line 232
  49. def OAI.MUB6.Certificate.PairSemantics.raw3758step0 line 234
  50. def OAI.MUB6.Certificate.PairSemantics.raw3758step1 line 236
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3758 line 238
  52. def OAI.MUB6.Certificate.PairSemantics.raw3759 line 251
  53. def OAI.MUB6.Certificate.PairSemantics.raw3759step0 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw3759step1 line 255
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3759 line 257
  56. def OAI.MUB6.Certificate.PairSemantics.raw3760 line 270
  57. def OAI.MUB6.Certificate.PairSemantics.raw3760step0 line 272
  58. def OAI.MUB6.Certificate.PairSemantics.raw3760step1 line 274
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3760 line 276
  60. def OAI.MUB6.Certificate.PairSemantics.raw3761 line 289
  61. def OAI.MUB6.Certificate.PairSemantics.raw3761step0 line 291
  62. def OAI.MUB6.Certificate.PairSemantics.raw3761step1 line 293
  63. def OAI.MUB6.Certificate.PairSemantics.raw3761step2 line 295
  64. def OAI.MUB6.Certificate.PairSemantics.raw3761step3 line 297
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3761 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw3762 line 321
  67. def OAI.MUB6.Certificate.PairSemantics.raw3762step0 line 323
  68. def OAI.MUB6.Certificate.PairSemantics.raw3762step1 line 325
  69. def OAI.MUB6.Certificate.PairSemantics.raw3762step2 line 327
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3762 line 329
  71. def OAI.MUB6.Certificate.PairSemantics.raw3763 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw3763step0 line 349
  73. def OAI.MUB6.Certificate.PairSemantics.raw3763step1 line 351
  74. def OAI.MUB6.Certificate.PairSemantics.raw3763step2 line 353
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3763 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw3764 line 373
  77. def OAI.MUB6.Certificate.PairSemantics.raw3764step0 line 375
  78. def OAI.MUB6.Certificate.PairSemantics.raw3764step1 line 377
  79. def OAI.MUB6.Certificate.PairSemantics.raw3764step2 line 379
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3764 line 381
  81. def OAI.MUB6.Certificate.PairSemantics.raw3765 line 399
  82. def OAI.MUB6.Certificate.PairSemantics.raw3765step0 line 401
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3765 line 403
  84. def OAI.MUB6.Certificate.PairSemantics.raw3766 line 412
  85. def OAI.MUB6.Certificate.PairSemantics.raw3766step0 line 414
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3766 line 416
  87. def OAI.MUB6.Certificate.PairSemantics.raw3767 line 425
  88. def OAI.MUB6.Certificate.PairSemantics.raw3767step0 line 427
  89. def OAI.MUB6.Certificate.PairSemantics.raw3767step1 line 429
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3767 line 431
  91. def OAI.MUB6.Certificate.PairSemantics.raw3768 line 444
  92. def OAI.MUB6.Certificate.PairSemantics.raw3768step0 line 446
  93. def OAI.MUB6.Certificate.PairSemantics.raw3768step1 line 448
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3768 line 450
  95. def OAI.MUB6.Certificate.PairSemantics.raw3769 line 463
  96. def OAI.MUB6.Certificate.PairSemantics.raw3769step0 line 465
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3769 line 467
  98. def OAI.MUB6.Certificate.PairSemantics.raw3770 line 476
  99. def OAI.MUB6.Certificate.PairSemantics.raw3770step0 line 478
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3770 line 480
  101. def OAI.MUB6.Certificate.PairSemantics.raw3771 line 489
  102. def OAI.MUB6.Certificate.PairSemantics.raw3771step0 line 491
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3771 line 493
  104. def OAI.MUB6.Certificate.PairSemantics.raw3772 line 502
  105. def OAI.MUB6.Certificate.PairSemantics.raw3772step0 line 504
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical3772 line 506
  107. def OAI.MUB6.Certificate.PairSemantics.raw3773 line 515
  108. def OAI.MUB6.Certificate.PairSemantics.raw3773step0 line 517
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3773 line 519
  110. def OAI.MUB6.Certificate.PairSemantics.raw3774 line 528
  111. def OAI.MUB6.Certificate.PairSemantics.raw3774step0 line 530
  112. def OAI.MUB6.Certificate.PairSemantics.raw3774step1 line 532
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical3774 line 534
  114. def OAI.MUB6.Certificate.PairSemantics.raw3775 line 547
  115. def OAI.MUB6.Certificate.PairSemantics.raw3775step0 line 549
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical3775 line 551