OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical269.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8608 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw8608step0 line 25
  3. def OAI.MUB6.Certificate.PairSemantics.raw8608step1 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw8608step2 line 29
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8608 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw8609 line 49
  7. def OAI.MUB6.Certificate.PairSemantics.raw8609step0 line 51
  8. def OAI.MUB6.Certificate.PairSemantics.raw8609step1 line 53
  9. def OAI.MUB6.Certificate.PairSemantics.raw8609step2 line 55
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8609 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw8610 line 75
  12. def OAI.MUB6.Certificate.PairSemantics.raw8610step0 line 77
  13. def OAI.MUB6.Certificate.PairSemantics.raw8610step1 line 79
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8610 line 81
  15. def OAI.MUB6.Certificate.PairSemantics.raw8611 line 95
  16. def OAI.MUB6.Certificate.PairSemantics.raw8611step0 line 97
  17. def OAI.MUB6.Certificate.PairSemantics.raw8611step1 line 99
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8611 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw8612 line 115
  20. def OAI.MUB6.Certificate.PairSemantics.raw8612step0 line 117
  21. def OAI.MUB6.Certificate.PairSemantics.raw8612step1 line 119
  22. def OAI.MUB6.Certificate.PairSemantics.raw8612step2 line 121
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8612 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw8613 line 141
  25. def OAI.MUB6.Certificate.PairSemantics.raw8613step0 line 143
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical8613 line 145
  27. def OAI.MUB6.Certificate.PairSemantics.raw8614 line 154
  28. def OAI.MUB6.Certificate.PairSemantics.raw8614step0 line 156
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8614 line 158
  30. def OAI.MUB6.Certificate.PairSemantics.raw8615 line 167
  31. def OAI.MUB6.Certificate.PairSemantics.raw8615step0 line 169
  32. def OAI.MUB6.Certificate.PairSemantics.raw8615step1 line 171
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8615 line 173
  34. def OAI.MUB6.Certificate.PairSemantics.raw8616 line 186
  35. def OAI.MUB6.Certificate.PairSemantics.raw8616step0 line 188
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical8616 line 190
  37. def OAI.MUB6.Certificate.PairSemantics.raw8617 line 199
  38. def OAI.MUB6.Certificate.PairSemantics.raw8617step0 line 201
  39. def OAI.MUB6.Certificate.PairSemantics.raw8617step1 line 203
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8617 line 205
  41. def OAI.MUB6.Certificate.PairSemantics.raw8618 line 219
  42. def OAI.MUB6.Certificate.PairSemantics.raw8618step0 line 221
  43. def OAI.MUB6.Certificate.PairSemantics.raw8618step1 line 223
  44. def OAI.MUB6.Certificate.PairSemantics.raw8618step2 line 225
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8618 line 227
  46. def OAI.MUB6.Certificate.PairSemantics.raw8619 line 245
  47. def OAI.MUB6.Certificate.PairSemantics.raw8619step0 line 247
  48. def OAI.MUB6.Certificate.PairSemantics.raw8619step1 line 249
  49. def OAI.MUB6.Certificate.PairSemantics.raw8619step2 line 251
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8619 line 253
  51. def OAI.MUB6.Certificate.PairSemantics.raw8620 line 271
  52. def OAI.MUB6.Certificate.PairSemantics.raw8620step0 line 273
  53. def OAI.MUB6.Certificate.PairSemantics.raw8620step1 line 275
  54. def OAI.MUB6.Certificate.PairSemantics.raw8620step2 line 277
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8620 line 279
  56. def OAI.MUB6.Certificate.PairSemantics.raw8621 line 297
  57. def OAI.MUB6.Certificate.PairSemantics.raw8621step0 line 299
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8621 line 301
  59. def OAI.MUB6.Certificate.PairSemantics.raw8622 line 310
  60. def OAI.MUB6.Certificate.PairSemantics.raw8622step0 line 312
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8622 line 314
  62. def OAI.MUB6.Certificate.PairSemantics.raw8623 line 323
  63. def OAI.MUB6.Certificate.PairSemantics.raw8623step0 line 325
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8623 line 327
  65. def OAI.MUB6.Certificate.PairSemantics.raw8624 line 336
  66. def OAI.MUB6.Certificate.PairSemantics.raw8624step0 line 338
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical8624 line 340
  68. def OAI.MUB6.Certificate.PairSemantics.raw8625 line 349
  69. def OAI.MUB6.Certificate.PairSemantics.raw8625step0 line 351
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8625 line 353
  71. def OAI.MUB6.Certificate.PairSemantics.raw8626 line 362
  72. def OAI.MUB6.Certificate.PairSemantics.raw8626step0 line 364
  73. def OAI.MUB6.Certificate.PairSemantics.raw8626step1 line 366
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical8626 line 368
  75. def OAI.MUB6.Certificate.PairSemantics.raw8627 line 383
  76. def OAI.MUB6.Certificate.PairSemantics.raw8627step0 line 385
  77. def OAI.MUB6.Certificate.PairSemantics.raw8627step1 line 387
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical8627 line 389
  79. def OAI.MUB6.Certificate.PairSemantics.raw8628 line 403
  80. def OAI.MUB6.Certificate.PairSemantics.raw8628step0 line 405
  81. def OAI.MUB6.Certificate.PairSemantics.raw8628step1 line 407
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8628 line 409
  83. def OAI.MUB6.Certificate.PairSemantics.raw8629 line 423
  84. def OAI.MUB6.Certificate.PairSemantics.raw8629step0 line 425
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8629 line 427
  86. def OAI.MUB6.Certificate.PairSemantics.raw8630 line 436
  87. def OAI.MUB6.Certificate.PairSemantics.raw8630step0 line 438
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8630 line 440
  89. def OAI.MUB6.Certificate.PairSemantics.raw8631 line 449
  90. def OAI.MUB6.Certificate.PairSemantics.raw8631step0 line 451
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8631 line 453
  92. def OAI.MUB6.Certificate.PairSemantics.raw8632 line 462
  93. def OAI.MUB6.Certificate.PairSemantics.raw8632step0 line 464
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8632 line 466
  95. def OAI.MUB6.Certificate.PairSemantics.raw8633 line 475
  96. def OAI.MUB6.Certificate.PairSemantics.raw8633step0 line 477
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical8633 line 479
  98. def OAI.MUB6.Certificate.PairSemantics.raw8634 line 488
  99. def OAI.MUB6.Certificate.PairSemantics.raw8634step0 line 490
  100. def OAI.MUB6.Certificate.PairSemantics.raw8634step1 line 492
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8634 line 494
  102. def OAI.MUB6.Certificate.PairSemantics.raw8635 line 508
  103. def OAI.MUB6.Certificate.PairSemantics.raw8635step0 line 510
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8635 line 512
  105. def OAI.MUB6.Certificate.PairSemantics.raw8636 line 521
  106. def OAI.MUB6.Certificate.PairSemantics.raw8636step0 line 523
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8636 line 525
  108. def OAI.MUB6.Certificate.PairSemantics.raw8637 line 534
  109. def OAI.MUB6.Certificate.PairSemantics.raw8637step0 line 536
  110. def OAI.MUB6.Certificate.PairSemantics.raw8637step1 line 538
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical8637 line 540
  112. def OAI.MUB6.Certificate.PairSemantics.raw8638 line 553
  113. def OAI.MUB6.Certificate.PairSemantics.raw8638step0 line 555
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8638 line 557
  115. def OAI.MUB6.Certificate.PairSemantics.raw8639 line 566
  116. def OAI.MUB6.Certificate.PairSemantics.raw8639step0 line 568
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical8639 line 570