OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical157.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5024 line 26
  2. def OAI.MUB6.Certificate.PairSemantics.raw5024step0 line 28
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5024 line 30
  4. def OAI.MUB6.Certificate.PairSemantics.raw5025 line 39
  5. def OAI.MUB6.Certificate.PairSemantics.raw5025step0 line 41
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5025 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw5026 line 52
  8. def OAI.MUB6.Certificate.PairSemantics.raw5026step0 line 54
  9. def OAI.MUB6.Certificate.PairSemantics.raw5026step1 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw5026step2 line 58
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5026 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw5027 line 77
  13. def OAI.MUB6.Certificate.PairSemantics.raw5027step0 line 79
  14. def OAI.MUB6.Certificate.PairSemantics.raw5027step1 line 81
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5027 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw5028 line 96
  17. def OAI.MUB6.Certificate.PairSemantics.raw5028step0 line 98
  18. def OAI.MUB6.Certificate.PairSemantics.raw5028step1 line 100
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5028 line 102
  20. def OAI.MUB6.Certificate.PairSemantics.raw5029 line 115
  21. def OAI.MUB6.Certificate.PairSemantics.raw5029step0 line 117
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5029 line 119
  23. def OAI.MUB6.Certificate.PairSemantics.raw5030 line 128
  24. def OAI.MUB6.Certificate.PairSemantics.raw5030step0 line 130
  25. def OAI.MUB6.Certificate.PairSemantics.raw5030step1 line 132
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5030 line 134
  27. def OAI.MUB6.Certificate.PairSemantics.raw5031 line 147
  28. def OAI.MUB6.Certificate.PairSemantics.raw5031step0 line 149
  29. def OAI.MUB6.Certificate.PairSemantics.raw5031step1 line 151
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5031 line 153
  31. def OAI.MUB6.Certificate.PairSemantics.raw5032 line 166
  32. def OAI.MUB6.Certificate.PairSemantics.raw5032step0 line 168
  33. def OAI.MUB6.Certificate.PairSemantics.raw5032step1 line 170
  34. def OAI.MUB6.Certificate.PairSemantics.raw5032step2 line 172
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5032 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw5033 line 191
  37. def OAI.MUB6.Certificate.PairSemantics.raw5033step0 line 193
  38. def OAI.MUB6.Certificate.PairSemantics.raw5033step1 line 195
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5033 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw5034 line 210
  41. def OAI.MUB6.Certificate.PairSemantics.raw5034step0 line 212
  42. def OAI.MUB6.Certificate.PairSemantics.raw5034step1 line 214
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5034 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw5035 line 229
  45. def OAI.MUB6.Certificate.PairSemantics.raw5035step0 line 231
  46. def OAI.MUB6.Certificate.PairSemantics.raw5035step1 line 233
  47. def OAI.MUB6.Certificate.PairSemantics.raw5035step2 line 235
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5035 line 237
  49. def OAI.MUB6.Certificate.PairSemantics.raw5036 line 254
  50. def OAI.MUB6.Certificate.PairSemantics.raw5036step0 line 256
  51. def OAI.MUB6.Certificate.PairSemantics.raw5036step1 line 258
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5036 line 260
  53. def OAI.MUB6.Certificate.PairSemantics.raw5037 line 273
  54. def OAI.MUB6.Certificate.PairSemantics.raw5037step0 line 275
  55. def OAI.MUB6.Certificate.PairSemantics.raw5037step1 line 277
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5037 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw5038 line 292
  58. def OAI.MUB6.Certificate.PairSemantics.raw5038step0 line 294
  59. def OAI.MUB6.Certificate.PairSemantics.raw5038step1 line 296
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5038 line 298
  61. def OAI.MUB6.Certificate.PairSemantics.raw5039 line 311
  62. def OAI.MUB6.Certificate.PairSemantics.raw5039step0 line 313
  63. def OAI.MUB6.Certificate.PairSemantics.raw5039step1 line 315
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5039 line 317
  65. def OAI.MUB6.Certificate.PairSemantics.raw5040 line 330
  66. def OAI.MUB6.Certificate.PairSemantics.raw5040step0 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw5040step1 line 334
  68. def OAI.MUB6.Certificate.PairSemantics.raw5040step2 line 336
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5040 line 338
  70. def OAI.MUB6.Certificate.PairSemantics.raw5041 line 355
  71. def OAI.MUB6.Certificate.PairSemantics.raw5041step0 line 357
  72. def OAI.MUB6.Certificate.PairSemantics.raw5041step1 line 359
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5041 line 361
  74. def OAI.MUB6.Certificate.PairSemantics.raw5042 line 374
  75. def OAI.MUB6.Certificate.PairSemantics.raw5042step0 line 376
  76. def OAI.MUB6.Certificate.PairSemantics.raw5042step1 line 378
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5042 line 380
  78. def OAI.MUB6.Certificate.PairSemantics.raw5043 line 393
  79. def OAI.MUB6.Certificate.PairSemantics.raw5043step0 line 395
  80. def OAI.MUB6.Certificate.PairSemantics.raw5043step1 line 397
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5043 line 399
  82. def OAI.MUB6.Certificate.PairSemantics.raw5044 line 412
  83. def OAI.MUB6.Certificate.PairSemantics.raw5044step0 line 414
  84. def OAI.MUB6.Certificate.PairSemantics.raw5044step1 line 416
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5044 line 418
  86. def OAI.MUB6.Certificate.PairSemantics.raw5045 line 431
  87. def OAI.MUB6.Certificate.PairSemantics.raw5045step0 line 433
  88. def OAI.MUB6.Certificate.PairSemantics.raw5045step1 line 435
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5045 line 437
  90. def OAI.MUB6.Certificate.PairSemantics.raw5046 line 450
  91. def OAI.MUB6.Certificate.PairSemantics.raw5046step0 line 452
  92. def OAI.MUB6.Certificate.PairSemantics.raw5046step1 line 454
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5046 line 456
  94. def OAI.MUB6.Certificate.PairSemantics.raw5047 line 469
  95. def OAI.MUB6.Certificate.PairSemantics.raw5047step0 line 471
  96. def OAI.MUB6.Certificate.PairSemantics.raw5047step1 line 473
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5047 line 475
  98. def OAI.MUB6.Certificate.PairSemantics.raw5048 line 488
  99. def OAI.MUB6.Certificate.PairSemantics.raw5048step0 line 490
  100. def OAI.MUB6.Certificate.PairSemantics.raw5048step1 line 492
  101. def OAI.MUB6.Certificate.PairSemantics.raw5048step2 line 494
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical5048 line 496
  103. def OAI.MUB6.Certificate.PairSemantics.raw5049 line 513
  104. def OAI.MUB6.Certificate.PairSemantics.raw5049step0 line 515
  105. def OAI.MUB6.Certificate.PairSemantics.raw5049step1 line 517
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical5049 line 519
  107. def OAI.MUB6.Certificate.PairSemantics.raw5050 line 532
  108. def OAI.MUB6.Certificate.PairSemantics.raw5050step0 line 534
  109. def OAI.MUB6.Certificate.PairSemantics.raw5050step1 line 536
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5050 line 538
  111. def OAI.MUB6.Certificate.PairSemantics.raw5051 line 551
  112. def OAI.MUB6.Certificate.PairSemantics.raw5051step0 line 553
  113. def OAI.MUB6.Certificate.PairSemantics.raw5051step1 line 555
  114. def OAI.MUB6.Certificate.PairSemantics.raw5051step2 line 557
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical5051 line 559
  116. def OAI.MUB6.Certificate.PairSemantics.raw5052 line 576
  117. def OAI.MUB6.Certificate.PairSemantics.raw5052step0 line 578
  118. def OAI.MUB6.Certificate.PairSemantics.raw5052step1 line 580
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical5052 line 582
  120. def OAI.MUB6.Certificate.PairSemantics.raw5053 line 595
  121. def OAI.MUB6.Certificate.PairSemantics.raw5053step0 line 597
  122. def OAI.MUB6.Certificate.PairSemantics.raw5053step1 line 599
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical5053 line 601
  124. def OAI.MUB6.Certificate.PairSemantics.raw5054 line 614
  125. def OAI.MUB6.Certificate.PairSemantics.raw5054step0 line 616
  126. def OAI.MUB6.Certificate.PairSemantics.raw5054step1 line 618
  127. def OAI.MUB6.Certificate.PairSemantics.raw5054step2 line 620
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical5054 line 622
  129. def OAI.MUB6.Certificate.PairSemantics.raw5055 line 639
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical5055 line 641