OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical297.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9504 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw9504step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9504 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw9505 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw9505step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9505 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw9506 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw9506step0 line 42
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9506 line 44
  10. def OAI.MUB6.Certificate.PairSemantics.raw9507 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw9507step0 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9507 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw9508 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw9508step0 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9508 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw9509 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw9509step0 line 81
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9509 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw9510 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw9510step0 line 94
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9510 line 96
  22. def OAI.MUB6.Certificate.PairSemantics.raw9511 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw9511step0 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw9511step1 line 109
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9511 line 111
  26. def OAI.MUB6.Certificate.PairSemantics.raw9512 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw9512step0 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw9512step1 line 129
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9512 line 131
  30. def OAI.MUB6.Certificate.PairSemantics.raw9513 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw9513step0 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw9513step1 line 149
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9513 line 151
  34. def OAI.MUB6.Certificate.PairSemantics.raw9514 line 164
  35. def OAI.MUB6.Certificate.PairSemantics.raw9514step0 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw9514step1 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9514 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw9515 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw9515step0 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw9515step1 line 187
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9515 line 189
  42. def OAI.MUB6.Certificate.PairSemantics.raw9516 line 202
  43. def OAI.MUB6.Certificate.PairSemantics.raw9516step0 line 204
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9516 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw9517 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw9517step0 line 217
  47. def OAI.MUB6.Certificate.PairSemantics.raw9517step1 line 219
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9517 line 221
  49. def OAI.MUB6.Certificate.PairSemantics.raw9518 line 234
  50. def OAI.MUB6.Certificate.PairSemantics.raw9518step0 line 236
  51. def OAI.MUB6.Certificate.PairSemantics.raw9518step1 line 238
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9518 line 240
  53. def OAI.MUB6.Certificate.PairSemantics.raw9519 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw9519step0 line 255
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9519 line 257
  56. def OAI.MUB6.Certificate.PairSemantics.raw9520 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw9520step0 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw9520step1 line 270
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9520 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw9521 line 285
  61. def OAI.MUB6.Certificate.PairSemantics.raw9521step0 line 287
  62. def OAI.MUB6.Certificate.PairSemantics.raw9521step1 line 289
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9521 line 291
  64. def OAI.MUB6.Certificate.PairSemantics.raw9522 line 304
  65. def OAI.MUB6.Certificate.PairSemantics.raw9522step0 line 306
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9522 line 308
  67. def OAI.MUB6.Certificate.PairSemantics.raw9523 line 317
  68. def OAI.MUB6.Certificate.PairSemantics.raw9523step0 line 319
  69. def OAI.MUB6.Certificate.PairSemantics.raw9523step1 line 321
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9523 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw9524 line 336
  72. def OAI.MUB6.Certificate.PairSemantics.raw9524step0 line 338
  73. def OAI.MUB6.Certificate.PairSemantics.raw9524step1 line 340
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9524 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw9525 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw9525step0 line 357
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9525 line 359
  78. def OAI.MUB6.Certificate.PairSemantics.raw9526 line 368
  79. def OAI.MUB6.Certificate.PairSemantics.raw9526step0 line 370
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical9526 line 372
  81. def OAI.MUB6.Certificate.PairSemantics.raw9527 line 381
  82. def OAI.MUB6.Certificate.PairSemantics.raw9527step0 line 383
  83. def OAI.MUB6.Certificate.PairSemantics.raw9527step1 line 385
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9527 line 387
  85. def OAI.MUB6.Certificate.PairSemantics.raw9528 line 400
  86. def OAI.MUB6.Certificate.PairSemantics.raw9528step0 line 402
  87. def OAI.MUB6.Certificate.PairSemantics.raw9528step1 line 404
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9528 line 406
  89. def OAI.MUB6.Certificate.PairSemantics.raw9529 line 419
  90. def OAI.MUB6.Certificate.PairSemantics.raw9529step0 line 421
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9529 line 423
  92. def OAI.MUB6.Certificate.PairSemantics.raw9530 line 432
  93. def OAI.MUB6.Certificate.PairSemantics.raw9530step0 line 434
  94. def OAI.MUB6.Certificate.PairSemantics.raw9530step1 line 436
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9530 line 438
  96. def OAI.MUB6.Certificate.PairSemantics.raw9531 line 451
  97. def OAI.MUB6.Certificate.PairSemantics.raw9531step0 line 453
  98. def OAI.MUB6.Certificate.PairSemantics.raw9531step1 line 455
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9531 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw9532 line 470
  101. def OAI.MUB6.Certificate.PairSemantics.raw9532step0 line 472
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9532 line 474
  103. def OAI.MUB6.Certificate.PairSemantics.raw9533 line 483
  104. def OAI.MUB6.Certificate.PairSemantics.raw9533step0 line 485
  105. def OAI.MUB6.Certificate.PairSemantics.raw9533step1 line 487
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical9533 line 489
  107. def OAI.MUB6.Certificate.PairSemantics.raw9534 line 502
  108. def OAI.MUB6.Certificate.PairSemantics.raw9534step0 line 504
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9534 line 506
  110. def OAI.MUB6.Certificate.PairSemantics.raw9535 line 515
  111. def OAI.MUB6.Certificate.PairSemantics.raw9535step0 line 517
  112. def OAI.MUB6.Certificate.PairSemantics.raw9535step1 line 519
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical9535 line 521