OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical78.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2496 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw2496step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw2496step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2496 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw2497 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw2497step0 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw2497step1 line 40
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2497 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw2498 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw2498step0 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw2498step1 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2498 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw2499 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw2499step0 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw2499step1 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw2499step2 line 80
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2499 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw2500 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw2500step0 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw2500step1 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw2500step2 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2500 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw2501 line 124
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2501 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw2502 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw2502step0 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw2502step1 line 134
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2502 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw2503 line 149
  30. def OAI.MUB6.Certificate.PairSemantics.raw2503step0 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw2503step1 line 153
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2503 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw2504 line 168
  34. def OAI.MUB6.Certificate.PairSemantics.raw2504step0 line 170
  35. def OAI.MUB6.Certificate.PairSemantics.raw2504step1 line 172
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2504 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw2505 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw2505step0 line 189
  39. def OAI.MUB6.Certificate.PairSemantics.raw2505step1 line 191
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2505 line 193
  41. def OAI.MUB6.Certificate.PairSemantics.raw2506 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw2506step0 line 208
  43. def OAI.MUB6.Certificate.PairSemantics.raw2506step1 line 210
  44. def OAI.MUB6.Certificate.PairSemantics.raw2506step2 line 212
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2506 line 214
  46. def OAI.MUB6.Certificate.PairSemantics.raw2507 line 231
  47. def OAI.MUB6.Certificate.PairSemantics.raw2507step0 line 233
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2507 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw2508 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw2508step0 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw2508step1 line 248
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2508 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw2509 line 263
  54. def OAI.MUB6.Certificate.PairSemantics.raw2509step0 line 265
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2509 line 267
  56. def OAI.MUB6.Certificate.PairSemantics.raw2510 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw2510step0 line 278
  58. def OAI.MUB6.Certificate.PairSemantics.raw2510step1 line 280
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2510 line 282
  60. def OAI.MUB6.Certificate.PairSemantics.raw2511 line 295
  61. def OAI.MUB6.Certificate.PairSemantics.raw2511step0 line 297
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2511 line 299
  63. def OAI.MUB6.Certificate.PairSemantics.raw2512 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw2512step0 line 310
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2512 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw2513 line 321
  67. def OAI.MUB6.Certificate.PairSemantics.raw2513step0 line 323
  68. def OAI.MUB6.Certificate.PairSemantics.raw2513step1 line 325
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2513 line 327
  70. def OAI.MUB6.Certificate.PairSemantics.raw2514 line 340
  71. def OAI.MUB6.Certificate.PairSemantics.raw2514step0 line 342
  72. def OAI.MUB6.Certificate.PairSemantics.raw2514step1 line 344
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical2514 line 346
  74. def OAI.MUB6.Certificate.PairSemantics.raw2515 line 359
  75. def OAI.MUB6.Certificate.PairSemantics.raw2515step0 line 361
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2515 line 363
  77. def OAI.MUB6.Certificate.PairSemantics.raw2516 line 372
  78. def OAI.MUB6.Certificate.PairSemantics.raw2516step0 line 374
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2516 line 376
  80. def OAI.MUB6.Certificate.PairSemantics.raw2517 line 385
  81. def OAI.MUB6.Certificate.PairSemantics.raw2517step0 line 387
  82. def OAI.MUB6.Certificate.PairSemantics.raw2517step1 line 389
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2517 line 391
  84. def OAI.MUB6.Certificate.PairSemantics.raw2518 line 404
  85. def OAI.MUB6.Certificate.PairSemantics.raw2518step0 line 406
  86. def OAI.MUB6.Certificate.PairSemantics.raw2518step1 line 408
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2518 line 410
  88. def OAI.MUB6.Certificate.PairSemantics.raw2519 line 423
  89. def OAI.MUB6.Certificate.PairSemantics.raw2519step0 line 425
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2519 line 427
  91. def OAI.MUB6.Certificate.PairSemantics.raw2520 line 436
  92. def OAI.MUB6.Certificate.PairSemantics.raw2520step0 line 438
  93. def OAI.MUB6.Certificate.PairSemantics.raw2520step1 line 440
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2520 line 442
  95. def OAI.MUB6.Certificate.PairSemantics.raw2521 line 455
  96. def OAI.MUB6.Certificate.PairSemantics.raw2521step0 line 457
  97. def OAI.MUB6.Certificate.PairSemantics.raw2521step1 line 459
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2521 line 461
  99. def OAI.MUB6.Certificate.PairSemantics.raw2522 line 474
  100. def OAI.MUB6.Certificate.PairSemantics.raw2522step0 line 476
  101. def OAI.MUB6.Certificate.PairSemantics.raw2522step1 line 478
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical2522 line 480
  103. def OAI.MUB6.Certificate.PairSemantics.raw2523 line 493
  104. def OAI.MUB6.Certificate.PairSemantics.raw2523step0 line 495
  105. def OAI.MUB6.Certificate.PairSemantics.raw2523step1 line 497
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical2523 line 499
  107. def OAI.MUB6.Certificate.PairSemantics.raw2524 line 512
  108. def OAI.MUB6.Certificate.PairSemantics.raw2524step0 line 514
  109. def OAI.MUB6.Certificate.PairSemantics.raw2524step1 line 516
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical2524 line 518
  111. def OAI.MUB6.Certificate.PairSemantics.raw2525 line 531
  112. def OAI.MUB6.Certificate.PairSemantics.raw2525step0 line 533
  113. def OAI.MUB6.Certificate.PairSemantics.raw2525step1 line 535
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical2525 line 537
  115. def OAI.MUB6.Certificate.PairSemantics.raw2526 line 550
  116. def OAI.MUB6.Certificate.PairSemantics.raw2526step0 line 552
  117. def OAI.MUB6.Certificate.PairSemantics.raw2526step1 line 554
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical2526 line 556
  119. def OAI.MUB6.Certificate.PairSemantics.raw2527 line 569
  120. def OAI.MUB6.Certificate.PairSemantics.raw2527step0 line 571
  121. def OAI.MUB6.Certificate.PairSemantics.raw2527step1 line 573
  122. def OAI.MUB6.Certificate.PairSemantics.raw2527step2 line 575
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical2527 line 577