OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical11.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw352 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw352step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical352 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw353 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw353step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical353 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw354 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw354step0 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw354step1 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical354 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw355 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw355step0 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw355step1 line 63
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical355 line 65
  15. def OAI.MUB6.Certificate.PairSemantics.raw356 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw356step0 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw356step1 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical356 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw357 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw357step0 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw357step1 line 101
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical357 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw358 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw358step0 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw358step1 line 120
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical358 line 122
  27. def OAI.MUB6.Certificate.PairSemantics.raw359 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw359step0 line 137
  29. def OAI.MUB6.Certificate.PairSemantics.raw359step1 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw359step2 line 141
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical359 line 143
  32. def OAI.MUB6.Certificate.PairSemantics.raw360 line 160
  33. def OAI.MUB6.Certificate.PairSemantics.raw360step0 line 162
  34. def OAI.MUB6.Certificate.PairSemantics.raw360step1 line 164
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical360 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw361 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw361step0 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw361step1 line 183
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical361 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw362 line 198
  41. def OAI.MUB6.Certificate.PairSemantics.raw362step0 line 200
  42. def OAI.MUB6.Certificate.PairSemantics.raw362step1 line 202
  43. def OAI.MUB6.Certificate.PairSemantics.raw362step2 line 204
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical362 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw363 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw363step0 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw363step1 line 227
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical363 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw364 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw364step0 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw364step1 line 246
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical364 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw365 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw365step0 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw365step1 line 265
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical365 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw366 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw366step0 line 282
  59. def OAI.MUB6.Certificate.PairSemantics.raw366step1 line 284
  60. def OAI.MUB6.Certificate.PairSemantics.raw366step2 line 286
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical366 line 288
  62. def OAI.MUB6.Certificate.PairSemantics.raw367 line 305
  63. def OAI.MUB6.Certificate.PairSemantics.raw367step0 line 307
  64. def OAI.MUB6.Certificate.PairSemantics.raw367step1 line 309
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical367 line 311
  66. def OAI.MUB6.Certificate.PairSemantics.raw368 line 324
  67. def OAI.MUB6.Certificate.PairSemantics.raw368step0 line 326
  68. def OAI.MUB6.Certificate.PairSemantics.raw368step1 line 328
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical368 line 330
  70. def OAI.MUB6.Certificate.PairSemantics.raw369 line 343
  71. def OAI.MUB6.Certificate.PairSemantics.raw369step0 line 345
  72. def OAI.MUB6.Certificate.PairSemantics.raw369step1 line 347
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical369 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw370 line 362
  75. def OAI.MUB6.Certificate.PairSemantics.raw370step0 line 364
  76. def OAI.MUB6.Certificate.PairSemantics.raw370step1 line 366
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical370 line 368
  78. def OAI.MUB6.Certificate.PairSemantics.raw371 line 381
  79. def OAI.MUB6.Certificate.PairSemantics.raw371step0 line 383
  80. def OAI.MUB6.Certificate.PairSemantics.raw371step1 line 385
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical371 line 387
  82. def OAI.MUB6.Certificate.PairSemantics.raw372 line 400
  83. def OAI.MUB6.Certificate.PairSemantics.raw372step0 line 402
  84. def OAI.MUB6.Certificate.PairSemantics.raw372step1 line 404
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical372 line 406
  86. def OAI.MUB6.Certificate.PairSemantics.raw373 line 419
  87. def OAI.MUB6.Certificate.PairSemantics.raw373step0 line 421
  88. def OAI.MUB6.Certificate.PairSemantics.raw373step1 line 423
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical373 line 425
  90. def OAI.MUB6.Certificate.PairSemantics.raw374 line 438
  91. def OAI.MUB6.Certificate.PairSemantics.raw374step0 line 440
  92. def OAI.MUB6.Certificate.PairSemantics.raw374step1 line 442
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical374 line 444
  94. def OAI.MUB6.Certificate.PairSemantics.raw375 line 457
  95. def OAI.MUB6.Certificate.PairSemantics.raw375step0 line 459
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical375 line 461
  97. def OAI.MUB6.Certificate.PairSemantics.raw376 line 470
  98. def OAI.MUB6.Certificate.PairSemantics.raw376step0 line 472
  99. def OAI.MUB6.Certificate.PairSemantics.raw376step1 line 474
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical376 line 476
  101. def OAI.MUB6.Certificate.PairSemantics.raw377 line 489
  102. def OAI.MUB6.Certificate.PairSemantics.raw377step0 line 491
  103. def OAI.MUB6.Certificate.PairSemantics.raw377step1 line 493
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical377 line 495
  105. def OAI.MUB6.Certificate.PairSemantics.raw378 line 508
  106. def OAI.MUB6.Certificate.PairSemantics.raw378step0 line 510
  107. def OAI.MUB6.Certificate.PairSemantics.raw378step1 line 512
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical378 line 514
  109. def OAI.MUB6.Certificate.PairSemantics.raw379 line 527
  110. def OAI.MUB6.Certificate.PairSemantics.raw379step0 line 529
  111. def OAI.MUB6.Certificate.PairSemantics.raw379step1 line 531
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical379 line 533
  113. def OAI.MUB6.Certificate.PairSemantics.raw380 line 546
  114. def OAI.MUB6.Certificate.PairSemantics.raw380step0 line 548
  115. def OAI.MUB6.Certificate.PairSemantics.raw380step1 line 550
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical380 line 552
  117. def OAI.MUB6.Certificate.PairSemantics.raw381 line 565
  118. def OAI.MUB6.Certificate.PairSemantics.raw381step0 line 567
  119. def OAI.MUB6.Certificate.PairSemantics.raw381step1 line 569
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical381 line 571
  121. def OAI.MUB6.Certificate.PairSemantics.raw382 line 584
  122. def OAI.MUB6.Certificate.PairSemantics.raw382step0 line 586
  123. def OAI.MUB6.Certificate.PairSemantics.raw382step1 line 588
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical382 line 590
  125. def OAI.MUB6.Certificate.PairSemantics.raw383 line 603
  126. def OAI.MUB6.Certificate.PairSemantics.raw383step0 line 605
  127. def OAI.MUB6.Certificate.PairSemantics.raw383step1 line 607
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical383 line 609