OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical144.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4608 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4608 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw4609 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw4609step0 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw4609step1 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw4609step2 line 30
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4609 line 32
  8. def OAI.MUB6.Certificate.PairSemantics.raw4610 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw4610step0 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw4610step1 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw4610step2 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4610 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw4611 line 74
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4611 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw4612 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw4612step0 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4612 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw4613 line 93
  19. def OAI.MUB6.Certificate.PairSemantics.raw4613step0 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw4613step1 line 97
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4613 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw4614 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw4614step0 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw4614step1 line 116
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4614 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw4615 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw4615step0 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw4615step1 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw4615step2 line 137
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4615 line 139
  31. def OAI.MUB6.Certificate.PairSemantics.raw4616 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw4616step0 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw4616step1 line 160
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4616 line 162
  35. def OAI.MUB6.Certificate.PairSemantics.raw4617 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw4617step0 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw4617step1 line 179
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4617 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw4618 line 194
  40. def OAI.MUB6.Certificate.PairSemantics.raw4618step0 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw4618step1 line 198
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4618 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw4619 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw4619step0 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw4619step1 line 217
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4619 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw4620 line 232
  48. def OAI.MUB6.Certificate.PairSemantics.raw4620step0 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw4620step1 line 236
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4620 line 238
  51. def OAI.MUB6.Certificate.PairSemantics.raw4621 line 251
  52. def OAI.MUB6.Certificate.PairSemantics.raw4621step0 line 253
  53. def OAI.MUB6.Certificate.PairSemantics.raw4621step1 line 255
  54. def OAI.MUB6.Certificate.PairSemantics.raw4621step2 line 257
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4621 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw4622 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw4622step0 line 278
  58. def OAI.MUB6.Certificate.PairSemantics.raw4622step1 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw4622step2 line 282
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical4622 line 284
  61. def OAI.MUB6.Certificate.PairSemantics.raw4623 line 301
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4623 line 303
  63. def OAI.MUB6.Certificate.PairSemantics.raw4624 line 307
  64. def OAI.MUB6.Certificate.PairSemantics.raw4624step0 line 309
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4624 line 311
  66. def OAI.MUB6.Certificate.PairSemantics.raw4625 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw4625step0 line 322
  68. def OAI.MUB6.Certificate.PairSemantics.raw4625step1 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw4625step2 line 326
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4625 line 328
  71. def OAI.MUB6.Certificate.PairSemantics.raw4626 line 345
  72. def OAI.MUB6.Certificate.PairSemantics.raw4626step0 line 347
  73. def OAI.MUB6.Certificate.PairSemantics.raw4626step1 line 349
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4626 line 351
  75. def OAI.MUB6.Certificate.PairSemantics.raw4627 line 364
  76. def OAI.MUB6.Certificate.PairSemantics.raw4627step0 line 366
  77. def OAI.MUB6.Certificate.PairSemantics.raw4627step1 line 368
  78. def OAI.MUB6.Certificate.PairSemantics.raw4627step2 line 370
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4627 line 372
  80. def OAI.MUB6.Certificate.PairSemantics.raw4628 line 389
  81. def OAI.MUB6.Certificate.PairSemantics.raw4628step0 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw4628step1 line 393
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4628 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw4629 line 408
  85. def OAI.MUB6.Certificate.PairSemantics.raw4629step0 line 410
  86. def OAI.MUB6.Certificate.PairSemantics.raw4629step1 line 412
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4629 line 414
  88. def OAI.MUB6.Certificate.PairSemantics.raw4630 line 427
  89. def OAI.MUB6.Certificate.PairSemantics.raw4630step0 line 429
  90. def OAI.MUB6.Certificate.PairSemantics.raw4630step1 line 431
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical4630 line 433
  92. def OAI.MUB6.Certificate.PairSemantics.raw4631 line 446
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4631 line 448
  94. def OAI.MUB6.Certificate.PairSemantics.raw4632 line 452
  95. def OAI.MUB6.Certificate.PairSemantics.raw4632step0 line 454
  96. def OAI.MUB6.Certificate.PairSemantics.raw4632step1 line 456
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4632 line 458
  98. def OAI.MUB6.Certificate.PairSemantics.raw4633 line 471
  99. def OAI.MUB6.Certificate.PairSemantics.raw4633step0 line 473
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4633 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw4634 line 484
  102. def OAI.MUB6.Certificate.PairSemantics.raw4634step0 line 486
  103. def OAI.MUB6.Certificate.PairSemantics.raw4634step1 line 488
  104. def OAI.MUB6.Certificate.PairSemantics.raw4634step2 line 490
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical4634 line 492
  106. def OAI.MUB6.Certificate.PairSemantics.raw4635 line 509
  107. def OAI.MUB6.Certificate.PairSemantics.raw4635step0 line 511
  108. def OAI.MUB6.Certificate.PairSemantics.raw4635step1 line 513
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical4635 line 515
  110. def OAI.MUB6.Certificate.PairSemantics.raw4636 line 528
  111. def OAI.MUB6.Certificate.PairSemantics.raw4636step0 line 530
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical4636 line 532
  113. def OAI.MUB6.Certificate.PairSemantics.raw4637 line 541
  114. def OAI.MUB6.Certificate.PairSemantics.raw4637step0 line 543
  115. def OAI.MUB6.Certificate.PairSemantics.raw4637step1 line 545
  116. def OAI.MUB6.Certificate.PairSemantics.raw4637step2 line 547
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical4637 line 549
  118. def OAI.MUB6.Certificate.PairSemantics.raw4638 line 566
  119. def OAI.MUB6.Certificate.PairSemantics.raw4638step0 line 568
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical4638 line 570
  121. def OAI.MUB6.Certificate.PairSemantics.raw4639 line 579
  122. def OAI.MUB6.Certificate.PairSemantics.raw4639step0 line 581
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical4639 line 583