OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical149.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4768 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4768step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw4768step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4768 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw4769 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw4769step0 line 41
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4769 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw4770 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw4770step0 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw4770step1 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4770 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw4771 line 71
  13. def OAI.MUB6.Certificate.PairSemantics.raw4771step0 line 73
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4771 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw4772 line 84
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4772 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw4773 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw4773step0 line 92
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4773 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw4774 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw4774step0 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4774 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw4775 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw4775step0 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw4775step1 line 120
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4775 line 122
  27. def OAI.MUB6.Certificate.PairSemantics.raw4776 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw4776step0 line 137
  29. def OAI.MUB6.Certificate.PairSemantics.raw4776step1 line 139
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4776 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw4777 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw4777step0 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw4777step1 line 158
  34. def OAI.MUB6.Certificate.PairSemantics.raw4777step2 line 160
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4777 line 162
  36. def OAI.MUB6.Certificate.PairSemantics.raw4778 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw4778step0 line 181
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4778 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw4779 line 192
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4779 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw4780 line 198
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4780 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw4781 line 204
  44. def OAI.MUB6.Certificate.PairSemantics.raw4781step0 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw4781step1 line 208
  46. def OAI.MUB6.Certificate.PairSemantics.raw4781step2 line 210
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4781 line 212
  48. def OAI.MUB6.Certificate.PairSemantics.raw4782 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw4782step0 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw4782step1 line 233
  51. def OAI.MUB6.Certificate.PairSemantics.raw4782step2 line 235
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4782 line 237
  53. def OAI.MUB6.Certificate.PairSemantics.raw4783 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw4783step0 line 256
  55. def OAI.MUB6.Certificate.PairSemantics.raw4783step1 line 258
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4783 line 260
  57. def OAI.MUB6.Certificate.PairSemantics.raw4784 line 273
  58. def OAI.MUB6.Certificate.PairSemantics.raw4784step0 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw4784step1 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw4784step2 line 279
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4784 line 281
  62. def OAI.MUB6.Certificate.PairSemantics.raw4785 line 298
  63. def OAI.MUB6.Certificate.PairSemantics.raw4785step0 line 300
  64. def OAI.MUB6.Certificate.PairSemantics.raw4785step1 line 302
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4785 line 304
  66. def OAI.MUB6.Certificate.PairSemantics.raw4786 line 317
  67. def OAI.MUB6.Certificate.PairSemantics.raw4786step0 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw4786step1 line 321
  69. def OAI.MUB6.Certificate.PairSemantics.raw4786step2 line 323
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4786 line 325
  71. def OAI.MUB6.Certificate.PairSemantics.raw4787 line 343
  72. def OAI.MUB6.Certificate.PairSemantics.raw4787step0 line 345
  73. def OAI.MUB6.Certificate.PairSemantics.raw4787step1 line 347
  74. def OAI.MUB6.Certificate.PairSemantics.raw4787step2 line 349
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4787 line 351
  76. def OAI.MUB6.Certificate.PairSemantics.raw4788 line 369
  77. def OAI.MUB6.Certificate.PairSemantics.raw4788step0 line 371
  78. def OAI.MUB6.Certificate.PairSemantics.raw4788step1 line 373
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4788 line 375
  80. def OAI.MUB6.Certificate.PairSemantics.raw4789 line 388
  81. def OAI.MUB6.Certificate.PairSemantics.raw4789step0 line 390
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4789 line 392
  83. def OAI.MUB6.Certificate.PairSemantics.raw4790 line 401
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4790 line 403
  85. def OAI.MUB6.Certificate.PairSemantics.raw4791 line 407
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4791 line 409
  87. def OAI.MUB6.Certificate.PairSemantics.raw4792 line 413
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4792 line 415
  89. def OAI.MUB6.Certificate.PairSemantics.raw4793 line 419
  90. def OAI.MUB6.Certificate.PairSemantics.raw4793step0 line 421
  91. def OAI.MUB6.Certificate.PairSemantics.raw4793step1 line 423
  92. def OAI.MUB6.Certificate.PairSemantics.raw4793step2 line 425
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4793 line 427
  94. def OAI.MUB6.Certificate.PairSemantics.raw4794 line 444
  95. def OAI.MUB6.Certificate.PairSemantics.raw4794step0 line 446
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4794 line 448
  97. def OAI.MUB6.Certificate.PairSemantics.raw4795 line 457
  98. def OAI.MUB6.Certificate.PairSemantics.raw4795step0 line 459
  99. def OAI.MUB6.Certificate.PairSemantics.raw4795step1 line 461
  100. def OAI.MUB6.Certificate.PairSemantics.raw4795step2 line 463
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4795 line 465
  102. def OAI.MUB6.Certificate.PairSemantics.raw4796 line 482
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4796 line 484
  104. def OAI.MUB6.Certificate.PairSemantics.raw4797 line 488
  105. def OAI.MUB6.Certificate.PairSemantics.raw4797step0 line 490
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical4797 line 492
  107. def OAI.MUB6.Certificate.PairSemantics.raw4798 line 501
  108. def OAI.MUB6.Certificate.PairSemantics.raw4798step0 line 503
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical4798 line 505
  110. def OAI.MUB6.Certificate.PairSemantics.raw4799 line 514
  111. def OAI.MUB6.Certificate.PairSemantics.raw4799step0 line 516
  112. def OAI.MUB6.Certificate.PairSemantics.raw4799step1 line 518
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical4799 line 520