OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical261.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8352 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw8352step0 line 25
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8352 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw8353 line 36
  5. def OAI.MUB6.Certificate.PairSemantics.raw8353step0 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw8353step1 line 40
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8353 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw8354 line 55
  9. def OAI.MUB6.Certificate.PairSemantics.raw8354step0 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw8354step1 line 59
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical8354 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw8355 line 74
  13. def OAI.MUB6.Certificate.PairSemantics.raw8355step0 line 76
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8355 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw8356 line 87
  16. def OAI.MUB6.Certificate.PairSemantics.raw8356step0 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw8356step1 line 91
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8356 line 93
  19. def OAI.MUB6.Certificate.PairSemantics.raw8357 line 106
  20. def OAI.MUB6.Certificate.PairSemantics.raw8357step0 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw8357step1 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw8357step2 line 112
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8357 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw8358 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw8358step0 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw8358step1 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw8358step2 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8358 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw8359 line 156
  30. def OAI.MUB6.Certificate.PairSemantics.raw8359step0 line 158
  31. def OAI.MUB6.Certificate.PairSemantics.raw8359step1 line 160
  32. def OAI.MUB6.Certificate.PairSemantics.raw8359step2 line 162
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8359 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw8360 line 181
  35. def OAI.MUB6.Certificate.PairSemantics.raw8360step0 line 183
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical8360 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw8361 line 194
  38. def OAI.MUB6.Certificate.PairSemantics.raw8361step0 line 196
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8361 line 198
  40. def OAI.MUB6.Certificate.PairSemantics.raw8362 line 207
  41. def OAI.MUB6.Certificate.PairSemantics.raw8362step0 line 209
  42. def OAI.MUB6.Certificate.PairSemantics.raw8362step1 line 211
  43. def OAI.MUB6.Certificate.PairSemantics.raw8362step2 line 213
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8362 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw8363 line 232
  46. def OAI.MUB6.Certificate.PairSemantics.raw8363step0 line 234
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8363 line 236
  48. def OAI.MUB6.Certificate.PairSemantics.raw8364 line 245
  49. def OAI.MUB6.Certificate.PairSemantics.raw8364step0 line 247
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8364 line 249
  51. def OAI.MUB6.Certificate.PairSemantics.raw8365 line 258
  52. def OAI.MUB6.Certificate.PairSemantics.raw8365step0 line 260
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8365 line 262
  54. def OAI.MUB6.Certificate.PairSemantics.raw8366 line 271
  55. def OAI.MUB6.Certificate.PairSemantics.raw8366step0 line 273
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8366 line 275
  57. def OAI.MUB6.Certificate.PairSemantics.raw8367 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw8367step0 line 286
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8367 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw8368 line 297
  61. def OAI.MUB6.Certificate.PairSemantics.raw8368step0 line 299
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8368 line 301
  63. def OAI.MUB6.Certificate.PairSemantics.raw8369 line 310
  64. def OAI.MUB6.Certificate.PairSemantics.raw8369step0 line 312
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8369 line 314
  66. def OAI.MUB6.Certificate.PairSemantics.raw8370 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw8370step0 line 325
  68. def OAI.MUB6.Certificate.PairSemantics.raw8370step1 line 327
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8370 line 329
  70. def OAI.MUB6.Certificate.PairSemantics.raw8371 line 342
  71. def OAI.MUB6.Certificate.PairSemantics.raw8371step0 line 344
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8371 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw8372 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw8372step0 line 357
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8372 line 359
  76. def OAI.MUB6.Certificate.PairSemantics.raw8373 line 368
  77. def OAI.MUB6.Certificate.PairSemantics.raw8373step0 line 370
  78. def OAI.MUB6.Certificate.PairSemantics.raw8373step1 line 372
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8373 line 374
  80. def OAI.MUB6.Certificate.PairSemantics.raw8374 line 387
  81. def OAI.MUB6.Certificate.PairSemantics.raw8374step0 line 389
  82. def OAI.MUB6.Certificate.PairSemantics.raw8374step1 line 391
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8374 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw8375 line 406
  85. def OAI.MUB6.Certificate.PairSemantics.raw8375step0 line 408
  86. def OAI.MUB6.Certificate.PairSemantics.raw8375step1 line 410
  87. def OAI.MUB6.Certificate.PairSemantics.raw8375step2 line 412
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8375 line 414
  89. def OAI.MUB6.Certificate.PairSemantics.raw8376 line 431
  90. def OAI.MUB6.Certificate.PairSemantics.raw8376step0 line 433
  91. def OAI.MUB6.Certificate.PairSemantics.raw8376step1 line 435
  92. def OAI.MUB6.Certificate.PairSemantics.raw8376step2 line 437
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8376 line 439
  94. def OAI.MUB6.Certificate.PairSemantics.raw8377 line 456
  95. def OAI.MUB6.Certificate.PairSemantics.raw8377step0 line 458
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8377 line 460
  97. def OAI.MUB6.Certificate.PairSemantics.raw8378 line 469
  98. def OAI.MUB6.Certificate.PairSemantics.raw8378step0 line 471
  99. def OAI.MUB6.Certificate.PairSemantics.raw8378step1 line 473
  100. def OAI.MUB6.Certificate.PairSemantics.raw8378step2 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw8378step3 line 477
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8378 line 479
  103. def OAI.MUB6.Certificate.PairSemantics.raw8379 line 501
  104. def OAI.MUB6.Certificate.PairSemantics.raw8379step0 line 503
  105. def OAI.MUB6.Certificate.PairSemantics.raw8379step1 line 505
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8379 line 507
  107. def OAI.MUB6.Certificate.PairSemantics.raw8380 line 520
  108. def OAI.MUB6.Certificate.PairSemantics.raw8380step0 line 522
  109. def OAI.MUB6.Certificate.PairSemantics.raw8380step1 line 524
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8380 line 526
  111. def OAI.MUB6.Certificate.PairSemantics.raw8381 line 539
  112. def OAI.MUB6.Certificate.PairSemantics.raw8381step0 line 541
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical8381 line 543
  114. def OAI.MUB6.Certificate.PairSemantics.raw8382 line 552
  115. def OAI.MUB6.Certificate.PairSemantics.raw8382step0 line 554
  116. def OAI.MUB6.Certificate.PairSemantics.raw8382step1 line 556
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical8382 line 558
  118. def OAI.MUB6.Certificate.PairSemantics.raw8383 line 571
  119. def OAI.MUB6.Certificate.PairSemantics.raw8383step0 line 573
  120. def OAI.MUB6.Certificate.PairSemantics.raw8383step1 line 575
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical8383 line 577