OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical289.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9248 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw9248step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw9248step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9248 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw9249 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw9249step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw9249step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9249 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw9250 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw9250step0 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw9250step1 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw9250step2 line 65
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9250 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw9251 line 84
  15. def OAI.MUB6.Certificate.PairSemantics.raw9251step0 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw9251step1 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw9251step2 line 90
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9251 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw9252 line 109
  20. def OAI.MUB6.Certificate.PairSemantics.raw9252step0 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw9252step1 line 113
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9252 line 115
  23. def OAI.MUB6.Certificate.PairSemantics.raw9253 line 128
  24. def OAI.MUB6.Certificate.PairSemantics.raw9253step0 line 130
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9253 line 132
  26. def OAI.MUB6.Certificate.PairSemantics.raw9254 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw9254step0 line 143
  28. def OAI.MUB6.Certificate.PairSemantics.raw9254step1 line 145
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9254 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw9255 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw9255step0 line 162
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical9255 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw9256 line 173
  34. def OAI.MUB6.Certificate.PairSemantics.raw9256step0 line 175
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9256 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw9257 line 186
  37. def OAI.MUB6.Certificate.PairSemantics.raw9257step0 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw9257step1 line 190
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9257 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw9258 line 205
  41. def OAI.MUB6.Certificate.PairSemantics.raw9258step0 line 207
  42. def OAI.MUB6.Certificate.PairSemantics.raw9258step1 line 209
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9258 line 211
  44. def OAI.MUB6.Certificate.PairSemantics.raw9259 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw9259step0 line 226
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9259 line 228
  47. def OAI.MUB6.Certificate.PairSemantics.raw9260 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw9260step0 line 239
  49. def OAI.MUB6.Certificate.PairSemantics.raw9260step1 line 241
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9260 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw9261 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw9261step0 line 258
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9261 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw9262 line 269
  55. def OAI.MUB6.Certificate.PairSemantics.raw9262step0 line 271
  56. def OAI.MUB6.Certificate.PairSemantics.raw9262step1 line 273
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9262 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw9263 line 288
  59. def OAI.MUB6.Certificate.PairSemantics.raw9263step0 line 290
  60. def OAI.MUB6.Certificate.PairSemantics.raw9263step1 line 292
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9263 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw9264 line 307
  63. def OAI.MUB6.Certificate.PairSemantics.raw9264step0 line 309
  64. def OAI.MUB6.Certificate.PairSemantics.raw9264step1 line 311
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9264 line 313
  66. def OAI.MUB6.Certificate.PairSemantics.raw9265 line 327
  67. def OAI.MUB6.Certificate.PairSemantics.raw9265step0 line 329
  68. def OAI.MUB6.Certificate.PairSemantics.raw9265step1 line 331
  69. def OAI.MUB6.Certificate.PairSemantics.raw9265step2 line 333
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9265 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw9266 line 353
  72. def OAI.MUB6.Certificate.PairSemantics.raw9266step0 line 355
  73. def OAI.MUB6.Certificate.PairSemantics.raw9266step1 line 357
  74. def OAI.MUB6.Certificate.PairSemantics.raw9266step2 line 359
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9266 line 361
  76. def OAI.MUB6.Certificate.PairSemantics.raw9267 line 379
  77. def OAI.MUB6.Certificate.PairSemantics.raw9267step0 line 381
  78. def OAI.MUB6.Certificate.PairSemantics.raw9267step1 line 383
  79. def OAI.MUB6.Certificate.PairSemantics.raw9267step2 line 385
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical9267 line 387
  81. def OAI.MUB6.Certificate.PairSemantics.raw9268 line 405
  82. def OAI.MUB6.Certificate.PairSemantics.raw9268step0 line 407
  83. def OAI.MUB6.Certificate.PairSemantics.raw9268step1 line 409
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9268 line 411
  85. def OAI.MUB6.Certificate.PairSemantics.raw9269 line 424
  86. def OAI.MUB6.Certificate.PairSemantics.raw9269step0 line 426
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9269 line 428
  88. def OAI.MUB6.Certificate.PairSemantics.raw9270 line 437
  89. def OAI.MUB6.Certificate.PairSemantics.raw9270step0 line 439
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical9270 line 441
  91. def OAI.MUB6.Certificate.PairSemantics.raw9271 line 450
  92. def OAI.MUB6.Certificate.PairSemantics.raw9271step0 line 452
  93. def OAI.MUB6.Certificate.PairSemantics.raw9271step1 line 454
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical9271 line 456
  95. def OAI.MUB6.Certificate.PairSemantics.raw9272 line 469
  96. def OAI.MUB6.Certificate.PairSemantics.raw9272step0 line 471
  97. def OAI.MUB6.Certificate.PairSemantics.raw9272step1 line 473
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9272 line 475
  99. def OAI.MUB6.Certificate.PairSemantics.raw9273 line 488
  100. def OAI.MUB6.Certificate.PairSemantics.raw9273step0 line 490
  101. def OAI.MUB6.Certificate.PairSemantics.raw9273step1 line 492
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9273 line 494
  103. def OAI.MUB6.Certificate.PairSemantics.raw9274 line 507
  104. def OAI.MUB6.Certificate.PairSemantics.raw9274step0 line 509
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical9274 line 511
  106. def OAI.MUB6.Certificate.PairSemantics.raw9275 line 520
  107. def OAI.MUB6.Certificate.PairSemantics.raw9275step0 line 522
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical9275 line 524
  109. def OAI.MUB6.Certificate.PairSemantics.raw9276 line 533
  110. def OAI.MUB6.Certificate.PairSemantics.raw9276step0 line 535
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical9276 line 537
  112. def OAI.MUB6.Certificate.PairSemantics.raw9277 line 546
  113. def OAI.MUB6.Certificate.PairSemantics.raw9277step0 line 548
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical9277 line 550
  115. def OAI.MUB6.Certificate.PairSemantics.raw9278 line 559
  116. def OAI.MUB6.Certificate.PairSemantics.raw9278step0 line 561
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical9278 line 563
  118. def OAI.MUB6.Certificate.PairSemantics.raw9279 line 572
  119. def OAI.MUB6.Certificate.PairSemantics.raw9279step0 line 574
  120. def OAI.MUB6.Certificate.PairSemantics.raw9279step1 line 576
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical9279 line 578