OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical150.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4800 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw4800step0 line 25
  3. def OAI.MUB6.Certificate.PairSemantics.raw4800step1 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw4800step2 line 29
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4800 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw4801 line 48
  7. def OAI.MUB6.Certificate.PairSemantics.raw4801step0 line 50
  8. def OAI.MUB6.Certificate.PairSemantics.raw4801step1 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw4801step2 line 54
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4801 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw4802 line 73
  12. def OAI.MUB6.Certificate.PairSemantics.raw4802step0 line 75
  13. def OAI.MUB6.Certificate.PairSemantics.raw4802step1 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw4802step2 line 79
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical4802 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw4803 line 98
  17. def OAI.MUB6.Certificate.PairSemantics.raw4803step0 line 100
  18. def OAI.MUB6.Certificate.PairSemantics.raw4803step1 line 102
  19. def OAI.MUB6.Certificate.PairSemantics.raw4803step2 line 104
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4803 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw4804 line 123
  22. def OAI.MUB6.Certificate.PairSemantics.raw4804step0 line 125
  23. def OAI.MUB6.Certificate.PairSemantics.raw4804step1 line 127
  24. def OAI.MUB6.Certificate.PairSemantics.raw4804step2 line 129
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4804 line 131
  26. def OAI.MUB6.Certificate.PairSemantics.raw4805 line 148
  27. def OAI.MUB6.Certificate.PairSemantics.raw4805step0 line 150
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4805 line 152
  29. def OAI.MUB6.Certificate.PairSemantics.raw4806 line 161
  30. def OAI.MUB6.Certificate.PairSemantics.raw4806step0 line 163
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4806 line 165
  32. def OAI.MUB6.Certificate.PairSemantics.raw4807 line 174
  33. def OAI.MUB6.Certificate.PairSemantics.raw4807step0 line 176
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4807 line 178
  35. def OAI.MUB6.Certificate.PairSemantics.raw4808 line 187
  36. def OAI.MUB6.Certificate.PairSemantics.raw4808step0 line 189
  37. def OAI.MUB6.Certificate.PairSemantics.raw4808step1 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw4808step2 line 193
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4808 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw4809 line 212
  41. def OAI.MUB6.Certificate.PairSemantics.raw4809step0 line 214
  42. def OAI.MUB6.Certificate.PairSemantics.raw4809step1 line 216
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4809 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw4810 line 231
  45. def OAI.MUB6.Certificate.PairSemantics.raw4810step0 line 233
  46. def OAI.MUB6.Certificate.PairSemantics.raw4810step1 line 235
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4810 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw4811 line 250
  49. def OAI.MUB6.Certificate.PairSemantics.raw4811step0 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw4811step1 line 254
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4811 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw4812 line 269
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4812 line 271
  54. def OAI.MUB6.Certificate.PairSemantics.raw4813 line 275
  55. def OAI.MUB6.Certificate.PairSemantics.raw4813step0 line 277
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4813 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw4814 line 288
  58. def OAI.MUB6.Certificate.PairSemantics.raw4814step0 line 290
  59. def OAI.MUB6.Certificate.PairSemantics.raw4814step1 line 292
  60. def OAI.MUB6.Certificate.PairSemantics.raw4814step2 line 294
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4814 line 296
  62. def OAI.MUB6.Certificate.PairSemantics.raw4815 line 313
  63. def OAI.MUB6.Certificate.PairSemantics.raw4815step0 line 315
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4815 line 317
  65. def OAI.MUB6.Certificate.PairSemantics.raw4816 line 326
  66. def OAI.MUB6.Certificate.PairSemantics.raw4816step0 line 328
  67. def OAI.MUB6.Certificate.PairSemantics.raw4816step1 line 330
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical4816 line 332
  69. def OAI.MUB6.Certificate.PairSemantics.raw4817 line 345
  70. def OAI.MUB6.Certificate.PairSemantics.raw4817step0 line 347
  71. def OAI.MUB6.Certificate.PairSemantics.raw4817step1 line 349
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4817 line 351
  73. def OAI.MUB6.Certificate.PairSemantics.raw4818 line 364
  74. def OAI.MUB6.Certificate.PairSemantics.raw4818step0 line 366
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4818 line 368
  76. def OAI.MUB6.Certificate.PairSemantics.raw4819 line 377
  77. def OAI.MUB6.Certificate.PairSemantics.raw4819step0 line 379
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical4819 line 381
  79. def OAI.MUB6.Certificate.PairSemantics.raw4820 line 390
  80. def OAI.MUB6.Certificate.PairSemantics.raw4820step0 line 392
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4820 line 394
  82. def OAI.MUB6.Certificate.PairSemantics.raw4821 line 403
  83. def OAI.MUB6.Certificate.PairSemantics.raw4821step0 line 405
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4821 line 407
  85. def OAI.MUB6.Certificate.PairSemantics.raw4822 line 416
  86. def OAI.MUB6.Certificate.PairSemantics.raw4822step0 line 418
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4822 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw4823 line 429
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4823 line 431
  90. def OAI.MUB6.Certificate.PairSemantics.raw4824 line 435
  91. def OAI.MUB6.Certificate.PairSemantics.raw4824step0 line 437
  92. def OAI.MUB6.Certificate.PairSemantics.raw4824step1 line 439
  93. def OAI.MUB6.Certificate.PairSemantics.raw4824step2 line 441
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4824 line 443
  95. def OAI.MUB6.Certificate.PairSemantics.raw4825 line 460
  96. def OAI.MUB6.Certificate.PairSemantics.raw4825step0 line 462
  97. def OAI.MUB6.Certificate.PairSemantics.raw4825step1 line 464
  98. def OAI.MUB6.Certificate.PairSemantics.raw4825step2 line 466
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical4825 line 468
  100. def OAI.MUB6.Certificate.PairSemantics.raw4826 line 485
  101. def OAI.MUB6.Certificate.PairSemantics.raw4826step0 line 487
  102. def OAI.MUB6.Certificate.PairSemantics.raw4826step1 line 489
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4826 line 491
  104. def OAI.MUB6.Certificate.PairSemantics.raw4827 line 504
  105. def OAI.MUB6.Certificate.PairSemantics.raw4827step0 line 506
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical4827 line 508
  107. def OAI.MUB6.Certificate.PairSemantics.raw4828 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw4828step0 line 519
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical4828 line 521
  110. def OAI.MUB6.Certificate.PairSemantics.raw4829 line 530
  111. def OAI.MUB6.Certificate.PairSemantics.raw4829step0 line 532
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical4829 line 534
  113. def OAI.MUB6.Certificate.PairSemantics.raw4830 line 543
  114. def OAI.MUB6.Certificate.PairSemantics.raw4830step0 line 545
  115. def OAI.MUB6.Certificate.PairSemantics.raw4830step1 line 547
  116. def OAI.MUB6.Certificate.PairSemantics.raw4830step2 line 549
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical4830 line 551
  118. def OAI.MUB6.Certificate.PairSemantics.raw4831 line 568
  119. def OAI.MUB6.Certificate.PairSemantics.raw4831step0 line 570
  120. def OAI.MUB6.Certificate.PairSemantics.raw4831step1 line 572
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical4831 line 574