OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical80.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2560 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw2560step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw2560step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2560 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw2561 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw2561step0 line 36
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2561 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw2562 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw2562step0 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2562 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw2563 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw2563step0 line 62
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2563 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw2564 line 73
  15. def OAI.MUB6.Certificate.PairSemantics.raw2564step0 line 75
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2564 line 77
  17. def OAI.MUB6.Certificate.PairSemantics.raw2565 line 86
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2565 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw2566 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw2566step0 line 94
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2566 line 96
  22. def OAI.MUB6.Certificate.PairSemantics.raw2567 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw2567step0 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw2567step1 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw2567step2 line 111
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical2567 line 113
  27. def OAI.MUB6.Certificate.PairSemantics.raw2568 line 131
  28. def OAI.MUB6.Certificate.PairSemantics.raw2568step0 line 133
  29. def OAI.MUB6.Certificate.PairSemantics.raw2568step1 line 135
  30. def OAI.MUB6.Certificate.PairSemantics.raw2568step2 line 137
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2568 line 139
  32. def OAI.MUB6.Certificate.PairSemantics.raw2569 line 157
  33. def OAI.MUB6.Certificate.PairSemantics.raw2569step0 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw2569step1 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw2569step2 line 163
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2569 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw2570 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw2570step0 line 185
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2570 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw2571 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw2571step0 line 198
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2571 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw2572 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw2572step0 line 211
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2572 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw2573 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw2573step0 line 224
  48. def OAI.MUB6.Certificate.PairSemantics.raw2573step1 line 226
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2573 line 228
  50. def OAI.MUB6.Certificate.PairSemantics.raw2574 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw2574step0 line 243
  52. def OAI.MUB6.Certificate.PairSemantics.raw2574step1 line 245
  53. def OAI.MUB6.Certificate.PairSemantics.raw2574step2 line 247
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2574 line 249
  55. def OAI.MUB6.Certificate.PairSemantics.raw2575 line 267
  56. def OAI.MUB6.Certificate.PairSemantics.raw2575step0 line 269
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2575 line 271
  58. def OAI.MUB6.Certificate.PairSemantics.raw2576 line 280
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2576 line 282
  60. def OAI.MUB6.Certificate.PairSemantics.raw2577 line 286
  61. def OAI.MUB6.Certificate.PairSemantics.raw2577step0 line 288
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2577 line 290
  63. def OAI.MUB6.Certificate.PairSemantics.raw2578 line 299
  64. def OAI.MUB6.Certificate.PairSemantics.raw2578step0 line 301
  65. def OAI.MUB6.Certificate.PairSemantics.raw2578step1 line 303
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2578 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw2579 line 318
  68. def OAI.MUB6.Certificate.PairSemantics.raw2579step0 line 320
  69. def OAI.MUB6.Certificate.PairSemantics.raw2579step1 line 322
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2579 line 324
  71. def OAI.MUB6.Certificate.PairSemantics.raw2580 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw2580step0 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw2580step1 line 341
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2580 line 343
  75. def OAI.MUB6.Certificate.PairSemantics.raw2581 line 356
  76. def OAI.MUB6.Certificate.PairSemantics.raw2581step0 line 358
  77. def OAI.MUB6.Certificate.PairSemantics.raw2581step1 line 360
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2581 line 362
  79. def OAI.MUB6.Certificate.PairSemantics.raw2582 line 375
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2582 line 377
  81. def OAI.MUB6.Certificate.PairSemantics.raw2583 line 381
  82. def OAI.MUB6.Certificate.PairSemantics.raw2583step0 line 383
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2583 line 385
  84. def OAI.MUB6.Certificate.PairSemantics.raw2584 line 394
  85. def OAI.MUB6.Certificate.PairSemantics.raw2584step0 line 396
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2584 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw2585 line 407
  88. def OAI.MUB6.Certificate.PairSemantics.raw2585step0 line 409
  89. def OAI.MUB6.Certificate.PairSemantics.raw2585step1 line 411
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2585 line 413
  91. def OAI.MUB6.Certificate.PairSemantics.raw2586 line 426
  92. def OAI.MUB6.Certificate.PairSemantics.raw2586step0 line 428
  93. def OAI.MUB6.Certificate.PairSemantics.raw2586step1 line 430
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2586 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw2587 line 445
  96. def OAI.MUB6.Certificate.PairSemantics.raw2587step0 line 447
  97. def OAI.MUB6.Certificate.PairSemantics.raw2587step1 line 449
  98. def OAI.MUB6.Certificate.PairSemantics.raw2587step2 line 451
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical2587 line 453
  100. def OAI.MUB6.Certificate.PairSemantics.raw2588 line 470
  101. def OAI.MUB6.Certificate.PairSemantics.raw2588step0 line 472
  102. def OAI.MUB6.Certificate.PairSemantics.raw2588step1 line 474
  103. def OAI.MUB6.Certificate.PairSemantics.raw2588step2 line 476
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical2588 line 478
  105. def OAI.MUB6.Certificate.PairSemantics.raw2589 line 496
  106. def OAI.MUB6.Certificate.PairSemantics.raw2589step0 line 498
  107. def OAI.MUB6.Certificate.PairSemantics.raw2589step1 line 500
  108. def OAI.MUB6.Certificate.PairSemantics.raw2589step2 line 502
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical2589 line 504
  110. def OAI.MUB6.Certificate.PairSemantics.raw2590 line 521
  111. def OAI.MUB6.Certificate.PairSemantics.raw2590step0 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw2590step1 line 525
  113. def OAI.MUB6.Certificate.PairSemantics.raw2590step2 line 527
  114. def OAI.MUB6.Certificate.PairSemantics.raw2590step3 line 529
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical2590 line 531
  116. def OAI.MUB6.Certificate.PairSemantics.raw2591 line 553
  117. def OAI.MUB6.Certificate.PairSemantics.raw2591step0 line 555
  118. def OAI.MUB6.Certificate.PairSemantics.raw2591step1 line 557
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical2591 line 559