OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical204.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6528 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw6528step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw6528step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6528 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw6529 line 36
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6529 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw6530 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6530 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw6531 line 48
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6531 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw6532 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw6532step0 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw6532step1 line 58
  14. def OAI.MUB6.Certificate.PairSemantics.raw6532step2 line 60
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6532 line 62
  16. def OAI.MUB6.Certificate.PairSemantics.raw6533 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw6533step0 line 81
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6533 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw6534 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw6534step0 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw6534step1 line 96
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6534 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw6535 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw6535step0 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw6535step1 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6535 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw6536 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw6536step0 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw6536step1 line 134
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6536 line 136
  31. def OAI.MUB6.Certificate.PairSemantics.raw6537 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw6537step0 line 151
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical6537 line 153
  34. def OAI.MUB6.Certificate.PairSemantics.raw6538 line 162
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6538 line 164
  36. def OAI.MUB6.Certificate.PairSemantics.raw6539 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6539 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw6540 line 174
  39. def OAI.MUB6.Certificate.PairSemantics.raw6540step0 line 176
  40. def OAI.MUB6.Certificate.PairSemantics.raw6540step1 line 178
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6540 line 180
  42. def OAI.MUB6.Certificate.PairSemantics.raw6541 line 193
  43. def OAI.MUB6.Certificate.PairSemantics.raw6541step0 line 195
  44. def OAI.MUB6.Certificate.PairSemantics.raw6541step1 line 197
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6541 line 199
  46. def OAI.MUB6.Certificate.PairSemantics.raw6542 line 212
  47. def OAI.MUB6.Certificate.PairSemantics.raw6542step0 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw6542step1 line 216
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6542 line 218
  50. def OAI.MUB6.Certificate.PairSemantics.raw6543 line 231
  51. def OAI.MUB6.Certificate.PairSemantics.raw6543step0 line 233
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6543 line 235
  53. def OAI.MUB6.Certificate.PairSemantics.raw6544 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw6544step0 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6544 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw6545 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw6545step0 line 260
  58. def OAI.MUB6.Certificate.PairSemantics.raw6545step1 line 262
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6545 line 264
  60. def OAI.MUB6.Certificate.PairSemantics.raw6546 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw6546step0 line 279
  62. def OAI.MUB6.Certificate.PairSemantics.raw6546step1 line 281
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6546 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw6547 line 296
  65. def OAI.MUB6.Certificate.PairSemantics.raw6547step0 line 298
  66. def OAI.MUB6.Certificate.PairSemantics.raw6547step1 line 300
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6547 line 302
  68. def OAI.MUB6.Certificate.PairSemantics.raw6548 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw6548step0 line 317
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6548 line 319
  71. def OAI.MUB6.Certificate.PairSemantics.raw6549 line 328
  72. def OAI.MUB6.Certificate.PairSemantics.raw6549step0 line 330
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6549 line 332
  74. def OAI.MUB6.Certificate.PairSemantics.raw6550 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw6550step0 line 343
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6550 line 345
  77. def OAI.MUB6.Certificate.PairSemantics.raw6551 line 354
  78. def OAI.MUB6.Certificate.PairSemantics.raw6551step0 line 356
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6551 line 358
  80. def OAI.MUB6.Certificate.PairSemantics.raw6552 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw6552step0 line 369
  82. def OAI.MUB6.Certificate.PairSemantics.raw6552step1 line 371
  83. def OAI.MUB6.Certificate.PairSemantics.raw6552step2 line 373
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6552 line 375
  85. def OAI.MUB6.Certificate.PairSemantics.raw6553 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw6553step0 line 394
  87. def OAI.MUB6.Certificate.PairSemantics.raw6553step1 line 396
  88. def OAI.MUB6.Certificate.PairSemantics.raw6553step2 line 398
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6553 line 400
  90. def OAI.MUB6.Certificate.PairSemantics.raw6554 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw6554step0 line 419
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical6554 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw6555 line 430
  94. def OAI.MUB6.Certificate.PairSemantics.raw6555step0 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw6555step1 line 434
  96. def OAI.MUB6.Certificate.PairSemantics.raw6555step2 line 436
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6555 line 438
  98. def OAI.MUB6.Certificate.PairSemantics.raw6556 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw6556step0 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw6556step1 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw6556step2 line 461
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical6556 line 463
  103. def OAI.MUB6.Certificate.PairSemantics.raw6557 line 480
  104. def OAI.MUB6.Certificate.PairSemantics.raw6557step0 line 482
  105. def OAI.MUB6.Certificate.PairSemantics.raw6557step1 line 484
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical6557 line 486
  107. def OAI.MUB6.Certificate.PairSemantics.raw6558 line 499
  108. def OAI.MUB6.Certificate.PairSemantics.raw6558step0 line 501
  109. def OAI.MUB6.Certificate.PairSemantics.raw6558step1 line 503
  110. def OAI.MUB6.Certificate.PairSemantics.raw6558step2 line 505
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical6558 line 507
  112. def OAI.MUB6.Certificate.PairSemantics.raw6559 line 524
  113. def OAI.MUB6.Certificate.PairSemantics.raw6559step0 line 526
  114. def OAI.MUB6.Certificate.PairSemantics.raw6559step1 line 528
  115. def OAI.MUB6.Certificate.PairSemantics.raw6559step2 line 530
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical6559 line 532