OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical167.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5344 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw5344step0 line 24
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5344 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw5345 line 35
  5. def OAI.MUB6.Certificate.PairSemantics.raw5345step0 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw5345step1 line 39
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical5345 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw5346 line 54
  9. def OAI.MUB6.Certificate.PairSemantics.raw5346step0 line 56
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical5346 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw5347 line 67
  12. def OAI.MUB6.Certificate.PairSemantics.raw5347step0 line 69
  13. def OAI.MUB6.Certificate.PairSemantics.raw5347step1 line 71
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5347 line 73
  15. def OAI.MUB6.Certificate.PairSemantics.raw5348 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw5348step0 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw5348step1 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw5348step2 line 92
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5348 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw5349 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw5349step0 line 113
  22. def OAI.MUB6.Certificate.PairSemantics.raw5349step1 line 115
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5349 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw5350 line 130
  25. def OAI.MUB6.Certificate.PairSemantics.raw5350step0 line 132
  26. def OAI.MUB6.Certificate.PairSemantics.raw5350step1 line 134
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5350 line 136
  28. def OAI.MUB6.Certificate.PairSemantics.raw5351 line 149
  29. def OAI.MUB6.Certificate.PairSemantics.raw5351step0 line 151
  30. def OAI.MUB6.Certificate.PairSemantics.raw5351step1 line 153
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5351 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw5352 line 168
  33. def OAI.MUB6.Certificate.PairSemantics.raw5352step0 line 170
  34. def OAI.MUB6.Certificate.PairSemantics.raw5352step1 line 172
  35. def OAI.MUB6.Certificate.PairSemantics.raw5352step2 line 174
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5352 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw5353 line 194
  38. def OAI.MUB6.Certificate.PairSemantics.raw5353step0 line 196
  39. def OAI.MUB6.Certificate.PairSemantics.raw5353step1 line 198
  40. def OAI.MUB6.Certificate.PairSemantics.raw5353step2 line 200
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5353 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw5354 line 220
  43. def OAI.MUB6.Certificate.PairSemantics.raw5354step0 line 222
  44. def OAI.MUB6.Certificate.PairSemantics.raw5354step1 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw5354step2 line 226
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5354 line 228
  47. def OAI.MUB6.Certificate.PairSemantics.raw5355 line 246
  48. def OAI.MUB6.Certificate.PairSemantics.raw5355step0 line 248
  49. def OAI.MUB6.Certificate.PairSemantics.raw5355step1 line 250
  50. def OAI.MUB6.Certificate.PairSemantics.raw5355step2 line 252
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5355 line 254
  52. def OAI.MUB6.Certificate.PairSemantics.raw5356 line 272
  53. def OAI.MUB6.Certificate.PairSemantics.raw5356step0 line 274
  54. def OAI.MUB6.Certificate.PairSemantics.raw5356step1 line 276
  55. def OAI.MUB6.Certificate.PairSemantics.raw5356step2 line 278
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5356 line 280
  57. def OAI.MUB6.Certificate.PairSemantics.raw5357 line 298
  58. def OAI.MUB6.Certificate.PairSemantics.raw5357step0 line 300
  59. def OAI.MUB6.Certificate.PairSemantics.raw5357step1 line 302
  60. def OAI.MUB6.Certificate.PairSemantics.raw5357step2 line 304
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5357 line 306
  62. def OAI.MUB6.Certificate.PairSemantics.raw5358 line 324
  63. def OAI.MUB6.Certificate.PairSemantics.raw5358step0 line 326
  64. def OAI.MUB6.Certificate.PairSemantics.raw5358step1 line 328
  65. def OAI.MUB6.Certificate.PairSemantics.raw5358step2 line 330
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5358 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw5359 line 350
  68. def OAI.MUB6.Certificate.PairSemantics.raw5359step0 line 352
  69. def OAI.MUB6.Certificate.PairSemantics.raw5359step1 line 354
  70. def OAI.MUB6.Certificate.PairSemantics.raw5359step2 line 356
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5359 line 358
  72. def OAI.MUB6.Certificate.PairSemantics.raw5360 line 376
  73. def OAI.MUB6.Certificate.PairSemantics.raw5360step0 line 378
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5360 line 380
  75. def OAI.MUB6.Certificate.PairSemantics.raw5361 line 389
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5361 line 391
  77. def OAI.MUB6.Certificate.PairSemantics.raw5362 line 395
  78. def OAI.MUB6.Certificate.PairSemantics.raw5362step0 line 397
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5362 line 399
  80. def OAI.MUB6.Certificate.PairSemantics.raw5363 line 408
  81. def OAI.MUB6.Certificate.PairSemantics.raw5363step0 line 410
  82. def OAI.MUB6.Certificate.PairSemantics.raw5363step1 line 412
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5363 line 414
  84. def OAI.MUB6.Certificate.PairSemantics.raw5364 line 427
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5364 line 429
  86. def OAI.MUB6.Certificate.PairSemantics.raw5365 line 433
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5365 line 435
  88. def OAI.MUB6.Certificate.PairSemantics.raw5366 line 439
  89. def OAI.MUB6.Certificate.PairSemantics.raw5366step0 line 441
  90. def OAI.MUB6.Certificate.PairSemantics.raw5366step1 line 443
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5366 line 445
  92. def OAI.MUB6.Certificate.PairSemantics.raw5367 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw5367step0 line 460
  94. def OAI.MUB6.Certificate.PairSemantics.raw5367step1 line 462
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical5367 line 464
  96. def OAI.MUB6.Certificate.PairSemantics.raw5368 line 477
  97. def OAI.MUB6.Certificate.PairSemantics.raw5368step0 line 479
  98. def OAI.MUB6.Certificate.PairSemantics.raw5368step1 line 481
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5368 line 483
  100. def OAI.MUB6.Certificate.PairSemantics.raw5369 line 496
  101. def OAI.MUB6.Certificate.PairSemantics.raw5369step0 line 498
  102. def OAI.MUB6.Certificate.PairSemantics.raw5369step1 line 500
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5369 line 502
  104. def OAI.MUB6.Certificate.PairSemantics.raw5370 line 515
  105. def OAI.MUB6.Certificate.PairSemantics.raw5370step0 line 517
  106. def OAI.MUB6.Certificate.PairSemantics.raw5370step1 line 519
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical5370 line 521
  108. def OAI.MUB6.Certificate.PairSemantics.raw5371 line 534
  109. def OAI.MUB6.Certificate.PairSemantics.raw5371step0 line 536
  110. def OAI.MUB6.Certificate.PairSemantics.raw5371step1 line 538
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical5371 line 540
  112. def OAI.MUB6.Certificate.PairSemantics.raw5372 line 553
  113. def OAI.MUB6.Certificate.PairSemantics.raw5372step0 line 555
  114. def OAI.MUB6.Certificate.PairSemantics.raw5372step1 line 557
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical5372 line 559
  116. def OAI.MUB6.Certificate.PairSemantics.raw5373 line 572
  117. def OAI.MUB6.Certificate.PairSemantics.raw5373step0 line 574
  118. def OAI.MUB6.Certificate.PairSemantics.raw5373step1 line 576
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical5373 line 578
  120. def OAI.MUB6.Certificate.PairSemantics.raw5374 line 591
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical5374 line 593
  122. def OAI.MUB6.Certificate.PairSemantics.raw5375 line 597
  123. def OAI.MUB6.Certificate.PairSemantics.raw5375step0 line 599
  124. def OAI.MUB6.Certificate.PairSemantics.raw5375step1 line 601
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical5375 line 603