OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical229.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7328 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw7328step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw7328step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7328 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw7329 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw7329step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw7329step1 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw7329step2 line 47
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7329 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw7330 line 67
  11. def OAI.MUB6.Certificate.PairSemantics.raw7330step0 line 69
  12. def OAI.MUB6.Certificate.PairSemantics.raw7330step1 line 71
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7330 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw7331 line 86
  15. def OAI.MUB6.Certificate.PairSemantics.raw7331step0 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw7331step1 line 90
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7331 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw7332 line 105
  19. def OAI.MUB6.Certificate.PairSemantics.raw7332step0 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw7332step1 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw7332step2 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7332 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7333 line 130
  24. def OAI.MUB6.Certificate.PairSemantics.raw7333step0 line 132
  25. def OAI.MUB6.Certificate.PairSemantics.raw7333step1 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw7333step2 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7333 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw7334 line 156
  29. def OAI.MUB6.Certificate.PairSemantics.raw7334step0 line 158
  30. def OAI.MUB6.Certificate.PairSemantics.raw7334step1 line 160
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7334 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw7335 line 175
  33. def OAI.MUB6.Certificate.PairSemantics.raw7335step0 line 177
  34. def OAI.MUB6.Certificate.PairSemantics.raw7335step1 line 179
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7335 line 181
  36. def OAI.MUB6.Certificate.PairSemantics.raw7336 line 194
  37. def OAI.MUB6.Certificate.PairSemantics.raw7336step0 line 196
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7336 line 198
  39. def OAI.MUB6.Certificate.PairSemantics.raw7337 line 207
  40. def OAI.MUB6.Certificate.PairSemantics.raw7337step0 line 209
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical7337 line 211
  42. def OAI.MUB6.Certificate.PairSemantics.raw7338 line 220
  43. def OAI.MUB6.Certificate.PairSemantics.raw7338step0 line 222
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7338 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw7339 line 233
  46. def OAI.MUB6.Certificate.PairSemantics.raw7339step0 line 235
  47. def OAI.MUB6.Certificate.PairSemantics.raw7339step1 line 237
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7339 line 239
  49. def OAI.MUB6.Certificate.PairSemantics.raw7340 line 252
  50. def OAI.MUB6.Certificate.PairSemantics.raw7340step0 line 254
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical7340 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw7341 line 265
  53. def OAI.MUB6.Certificate.PairSemantics.raw7341step0 line 267
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7341 line 269
  55. def OAI.MUB6.Certificate.PairSemantics.raw7342 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw7342step0 line 280
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7342 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw7343 line 291
  59. def OAI.MUB6.Certificate.PairSemantics.raw7343step0 line 293
  60. def OAI.MUB6.Certificate.PairSemantics.raw7343step1 line 295
  61. def OAI.MUB6.Certificate.PairSemantics.raw7343step2 line 297
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7343 line 299
  63. def OAI.MUB6.Certificate.PairSemantics.raw7344 line 316
  64. def OAI.MUB6.Certificate.PairSemantics.raw7344step0 line 318
  65. def OAI.MUB6.Certificate.PairSemantics.raw7344step1 line 320
  66. def OAI.MUB6.Certificate.PairSemantics.raw7344step2 line 322
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical7344 line 324
  68. def OAI.MUB6.Certificate.PairSemantics.raw7345 line 341
  69. def OAI.MUB6.Certificate.PairSemantics.raw7345step0 line 343
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7345 line 345
  71. def OAI.MUB6.Certificate.PairSemantics.raw7346 line 354
  72. def OAI.MUB6.Certificate.PairSemantics.raw7346step0 line 356
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical7346 line 358
  74. def OAI.MUB6.Certificate.PairSemantics.raw7347 line 367
  75. def OAI.MUB6.Certificate.PairSemantics.raw7347step0 line 369
  76. def OAI.MUB6.Certificate.PairSemantics.raw7347step1 line 371
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical7347 line 373
  78. def OAI.MUB6.Certificate.PairSemantics.raw7348 line 386
  79. def OAI.MUB6.Certificate.PairSemantics.raw7348step0 line 388
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7348 line 390
  81. def OAI.MUB6.Certificate.PairSemantics.raw7349 line 399
  82. def OAI.MUB6.Certificate.PairSemantics.raw7349step0 line 401
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7349 line 403
  84. def OAI.MUB6.Certificate.PairSemantics.raw7350 line 412
  85. def OAI.MUB6.Certificate.PairSemantics.raw7350step0 line 414
  86. def OAI.MUB6.Certificate.PairSemantics.raw7350step1 line 416
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7350 line 418
  88. def OAI.MUB6.Certificate.PairSemantics.raw7351 line 431
  89. def OAI.MUB6.Certificate.PairSemantics.raw7351step0 line 433
  90. def OAI.MUB6.Certificate.PairSemantics.raw7351step1 line 435
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7351 line 437
  92. def OAI.MUB6.Certificate.PairSemantics.raw7352 line 450
  93. def OAI.MUB6.Certificate.PairSemantics.raw7352step0 line 452
  94. def OAI.MUB6.Certificate.PairSemantics.raw7352step1 line 454
  95. def OAI.MUB6.Certificate.PairSemantics.raw7352step2 line 456
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7352 line 458
  97. def OAI.MUB6.Certificate.PairSemantics.raw7353 line 475
  98. def OAI.MUB6.Certificate.PairSemantics.raw7353step0 line 477
  99. def OAI.MUB6.Certificate.PairSemantics.raw7353step1 line 479
  100. def OAI.MUB6.Certificate.PairSemantics.raw7353step2 line 481
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7353 line 483
  102. def OAI.MUB6.Certificate.PairSemantics.raw7354 line 500
  103. def OAI.MUB6.Certificate.PairSemantics.raw7354step0 line 502
  104. def OAI.MUB6.Certificate.PairSemantics.raw7354step1 line 504
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7354 line 506
  106. def OAI.MUB6.Certificate.PairSemantics.raw7355 line 519
  107. def OAI.MUB6.Certificate.PairSemantics.raw7355step0 line 521
  108. def OAI.MUB6.Certificate.PairSemantics.raw7355step1 line 523
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical7355 line 525
  110. def OAI.MUB6.Certificate.PairSemantics.raw7356 line 538
  111. def OAI.MUB6.Certificate.PairSemantics.raw7356step0 line 540
  112. def OAI.MUB6.Certificate.PairSemantics.raw7356step1 line 542
  113. def OAI.MUB6.Certificate.PairSemantics.raw7356step2 line 544
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical7356 line 546
  115. def OAI.MUB6.Certificate.PairSemantics.raw7357 line 563
  116. def OAI.MUB6.Certificate.PairSemantics.raw7357step0 line 565
  117. def OAI.MUB6.Certificate.PairSemantics.raw7357step1 line 567
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7357 line 569
  119. def OAI.MUB6.Certificate.PairSemantics.raw7358 line 582
  120. def OAI.MUB6.Certificate.PairSemantics.raw7358step0 line 584
  121. def OAI.MUB6.Certificate.PairSemantics.raw7358step1 line 586
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical7358 line 588
  123. def OAI.MUB6.Certificate.PairSemantics.raw7359 line 601
  124. def OAI.MUB6.Certificate.PairSemantics.raw7359step0 line 603
  125. def OAI.MUB6.Certificate.PairSemantics.raw7359step1 line 605
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical7359 line 607