OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical138.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4416 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw4416step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw4416step1 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw4416step2 line 25
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4416 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw4417 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw4417step0 line 46
  8. def OAI.MUB6.Certificate.PairSemantics.raw4417step1 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4417 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw4418 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw4418step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw4418step1 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4418 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw4419 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw4419step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw4419step1 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw4419step2 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4419 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw4420 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw4420step0 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw4420step1 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw4420step2 line 113
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4420 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw4421 line 132
  25. def OAI.MUB6.Certificate.PairSemantics.raw4421step0 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw4421step1 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4421 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw4422 line 151
  29. def OAI.MUB6.Certificate.PairSemantics.raw4422step0 line 153
  30. def OAI.MUB6.Certificate.PairSemantics.raw4422step1 line 155
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4422 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw4423 line 170
  33. def OAI.MUB6.Certificate.PairSemantics.raw4423step0 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw4423step1 line 174
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4423 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw4424 line 189
  37. def OAI.MUB6.Certificate.PairSemantics.raw4424step0 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw4424step1 line 193
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4424 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw4425 line 208
  41. def OAI.MUB6.Certificate.PairSemantics.raw4425step0 line 210
  42. def OAI.MUB6.Certificate.PairSemantics.raw4425step1 line 212
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4425 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw4426 line 227
  45. def OAI.MUB6.Certificate.PairSemantics.raw4426step0 line 229
  46. def OAI.MUB6.Certificate.PairSemantics.raw4426step1 line 231
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4426 line 233
  48. def OAI.MUB6.Certificate.PairSemantics.raw4427 line 246
  49. def OAI.MUB6.Certificate.PairSemantics.raw4427step0 line 248
  50. def OAI.MUB6.Certificate.PairSemantics.raw4427step1 line 250
  51. def OAI.MUB6.Certificate.PairSemantics.raw4427step2 line 252
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4427 line 254
  53. def OAI.MUB6.Certificate.PairSemantics.raw4428 line 271
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4428 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw4429 line 277
  56. def OAI.MUB6.Certificate.PairSemantics.raw4429step0 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw4429step1 line 281
  58. def OAI.MUB6.Certificate.PairSemantics.raw4429step2 line 283
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4429 line 285
  60. def OAI.MUB6.Certificate.PairSemantics.raw4430 line 302
  61. def OAI.MUB6.Certificate.PairSemantics.raw4430step0 line 304
  62. def OAI.MUB6.Certificate.PairSemantics.raw4430step1 line 306
  63. def OAI.MUB6.Certificate.PairSemantics.raw4430step2 line 308
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4430 line 310
  65. def OAI.MUB6.Certificate.PairSemantics.raw4431 line 327
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4431 line 329
  67. def OAI.MUB6.Certificate.PairSemantics.raw4432 line 333
  68. def OAI.MUB6.Certificate.PairSemantics.raw4432step0 line 335
  69. def OAI.MUB6.Certificate.PairSemantics.raw4432step1 line 337
  70. def OAI.MUB6.Certificate.PairSemantics.raw4432step2 line 339
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4432 line 341
  72. def OAI.MUB6.Certificate.PairSemantics.raw4433 line 358
  73. def OAI.MUB6.Certificate.PairSemantics.raw4433step0 line 360
  74. def OAI.MUB6.Certificate.PairSemantics.raw4433step1 line 362
  75. def OAI.MUB6.Certificate.PairSemantics.raw4433step2 line 364
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4433 line 366
  77. def OAI.MUB6.Certificate.PairSemantics.raw4434 line 383
  78. def OAI.MUB6.Certificate.PairSemantics.raw4434step0 line 385
  79. def OAI.MUB6.Certificate.PairSemantics.raw4434step1 line 387
  80. def OAI.MUB6.Certificate.PairSemantics.raw4434step2 line 389
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4434 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw4435 line 408
  83. def OAI.MUB6.Certificate.PairSemantics.raw4435step0 line 410
  84. def OAI.MUB6.Certificate.PairSemantics.raw4435step1 line 412
  85. def OAI.MUB6.Certificate.PairSemantics.raw4435step2 line 414
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4435 line 416
  87. def OAI.MUB6.Certificate.PairSemantics.raw4436 line 433
  88. def OAI.MUB6.Certificate.PairSemantics.raw4436step0 line 435
  89. def OAI.MUB6.Certificate.PairSemantics.raw4436step1 line 437
  90. def OAI.MUB6.Certificate.PairSemantics.raw4436step2 line 439
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical4436 line 441
  92. def OAI.MUB6.Certificate.PairSemantics.raw4437 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw4437step0 line 460
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4437 line 462
  95. def OAI.MUB6.Certificate.PairSemantics.raw4438 line 471
  96. def OAI.MUB6.Certificate.PairSemantics.raw4438step0 line 473
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4438 line 475
  98. def OAI.MUB6.Certificate.PairSemantics.raw4439 line 484
  99. def OAI.MUB6.Certificate.PairSemantics.raw4439step0 line 486
  100. def OAI.MUB6.Certificate.PairSemantics.raw4439step1 line 488
  101. def OAI.MUB6.Certificate.PairSemantics.raw4439step2 line 490
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4439 line 492
  103. def OAI.MUB6.Certificate.PairSemantics.raw4440 line 509
  104. def OAI.MUB6.Certificate.PairSemantics.raw4440step0 line 511
  105. def OAI.MUB6.Certificate.PairSemantics.raw4440step1 line 513
  106. def OAI.MUB6.Certificate.PairSemantics.raw4440step2 line 515
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical4440 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw4441 line 534
  109. def OAI.MUB6.Certificate.PairSemantics.raw4441step0 line 536
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical4441 line 538
  111. def OAI.MUB6.Certificate.PairSemantics.raw4442 line 547
  112. def OAI.MUB6.Certificate.PairSemantics.raw4442step0 line 549
  113. def OAI.MUB6.Certificate.PairSemantics.raw4442step1 line 551
  114. def OAI.MUB6.Certificate.PairSemantics.raw4442step2 line 553
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical4442 line 555
  116. def OAI.MUB6.Certificate.PairSemantics.raw4443 line 572
  117. def OAI.MUB6.Certificate.PairSemantics.raw4443step0 line 574
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical4443 line 576
  119. def OAI.MUB6.Certificate.PairSemantics.raw4444 line 585
  120. def OAI.MUB6.Certificate.PairSemantics.raw4444step0 line 587
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical4444 line 589
  122. def OAI.MUB6.Certificate.PairSemantics.raw4445 line 598
  123. def OAI.MUB6.Certificate.PairSemantics.raw4445step0 line 600
  124. def OAI.MUB6.Certificate.PairSemantics.raw4445step1 line 602
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical4445 line 604
  126. def OAI.MUB6.Certificate.PairSemantics.raw4446 line 617
  127. def OAI.MUB6.Certificate.PairSemantics.raw4446step0 line 619
  128. def OAI.MUB6.Certificate.PairSemantics.raw4446step1 line 621
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical4446 line 623
  130. def OAI.MUB6.Certificate.PairSemantics.raw4447 line 636
  131. def OAI.MUB6.Certificate.PairSemantics.raw4447step0 line 638
  132. def OAI.MUB6.Certificate.PairSemantics.raw4447step1 line 640
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical4447 line 642