OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical130.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4160 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw4160step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw4160step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4160 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw4161 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw4161step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw4161step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4161 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw4162 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw4162step0 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw4162step1 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw4162step2 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4162 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw4163 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw4163step0 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw4163step1 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw4163step2 line 85
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4163 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw4164 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw4164step0 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw4164step1 line 108
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4164 line 110
  23. def OAI.MUB6.Certificate.PairSemantics.raw4165 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw4165step0 line 125
  25. def OAI.MUB6.Certificate.PairSemantics.raw4165step1 line 127
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4165 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw4166 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw4166step0 line 144
  29. def OAI.MUB6.Certificate.PairSemantics.raw4166step1 line 146
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4166 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw4167 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw4167step0 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw4167step1 line 165
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4167 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw4168 line 180
  36. def OAI.MUB6.Certificate.PairSemantics.raw4168step0 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw4168step1 line 184
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4168 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw4169 line 199
  40. def OAI.MUB6.Certificate.PairSemantics.raw4169step0 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw4169step1 line 203
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4169 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw4170 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw4170step0 line 220
  45. def OAI.MUB6.Certificate.PairSemantics.raw4170step1 line 222
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4170 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw4171 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw4171step0 line 239
  49. def OAI.MUB6.Certificate.PairSemantics.raw4171step1 line 241
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4171 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw4172 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw4172step0 line 258
  53. def OAI.MUB6.Certificate.PairSemantics.raw4172step1 line 260
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4172 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw4173 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw4173step0 line 277
  57. def OAI.MUB6.Certificate.PairSemantics.raw4173step1 line 279
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4173 line 281
  59. def OAI.MUB6.Certificate.PairSemantics.raw4174 line 294
  60. def OAI.MUB6.Certificate.PairSemantics.raw4174step0 line 296
  61. def OAI.MUB6.Certificate.PairSemantics.raw4174step1 line 298
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4174 line 300
  63. def OAI.MUB6.Certificate.PairSemantics.raw4175 line 313
  64. def OAI.MUB6.Certificate.PairSemantics.raw4175step0 line 315
  65. def OAI.MUB6.Certificate.PairSemantics.raw4175step1 line 317
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4175 line 319
  67. def OAI.MUB6.Certificate.PairSemantics.raw4176 line 332
  68. def OAI.MUB6.Certificate.PairSemantics.raw4176step0 line 334
  69. def OAI.MUB6.Certificate.PairSemantics.raw4176step1 line 336
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4176 line 338
  71. def OAI.MUB6.Certificate.PairSemantics.raw4177 line 351
  72. def OAI.MUB6.Certificate.PairSemantics.raw4177step0 line 353
  73. def OAI.MUB6.Certificate.PairSemantics.raw4177step1 line 355
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4177 line 357
  75. def OAI.MUB6.Certificate.PairSemantics.raw4178 line 370
  76. def OAI.MUB6.Certificate.PairSemantics.raw4178step0 line 372
  77. def OAI.MUB6.Certificate.PairSemantics.raw4178step1 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw4178step2 line 376
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4178 line 378
  80. def OAI.MUB6.Certificate.PairSemantics.raw4179 line 395
  81. def OAI.MUB6.Certificate.PairSemantics.raw4179step0 line 397
  82. def OAI.MUB6.Certificate.PairSemantics.raw4179step1 line 399
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4179 line 401
  84. def OAI.MUB6.Certificate.PairSemantics.raw4180 line 414
  85. def OAI.MUB6.Certificate.PairSemantics.raw4180step0 line 416
  86. def OAI.MUB6.Certificate.PairSemantics.raw4180step1 line 418
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4180 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw4181 line 433
  89. def OAI.MUB6.Certificate.PairSemantics.raw4181step0 line 435
  90. def OAI.MUB6.Certificate.PairSemantics.raw4181step1 line 437
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical4181 line 439
  92. def OAI.MUB6.Certificate.PairSemantics.raw4182 line 452
  93. def OAI.MUB6.Certificate.PairSemantics.raw4182step0 line 454
  94. def OAI.MUB6.Certificate.PairSemantics.raw4182step1 line 456
  95. def OAI.MUB6.Certificate.PairSemantics.raw4182step2 line 458
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4182 line 460
  97. def OAI.MUB6.Certificate.PairSemantics.raw4183 line 477
  98. def OAI.MUB6.Certificate.PairSemantics.raw4183step0 line 479
  99. def OAI.MUB6.Certificate.PairSemantics.raw4183step1 line 481
  100. def OAI.MUB6.Certificate.PairSemantics.raw4183step2 line 483
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4183 line 485
  102. def OAI.MUB6.Certificate.PairSemantics.raw4184 line 502
  103. def OAI.MUB6.Certificate.PairSemantics.raw4184step0 line 504
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4184 line 506
  105. def OAI.MUB6.Certificate.PairSemantics.raw4185 line 515
  106. def OAI.MUB6.Certificate.PairSemantics.raw4185step0 line 517
  107. def OAI.MUB6.Certificate.PairSemantics.raw4185step1 line 519
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4185 line 521
  109. def OAI.MUB6.Certificate.PairSemantics.raw4186 line 534
  110. def OAI.MUB6.Certificate.PairSemantics.raw4186step0 line 536
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical4186 line 538
  112. def OAI.MUB6.Certificate.PairSemantics.raw4187 line 547
  113. def OAI.MUB6.Certificate.PairSemantics.raw4187step0 line 549
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical4187 line 551
  115. def OAI.MUB6.Certificate.PairSemantics.raw4188 line 560
  116. def OAI.MUB6.Certificate.PairSemantics.raw4188step0 line 562
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical4188 line 564
  118. def OAI.MUB6.Certificate.PairSemantics.raw4189 line 573
  119. def OAI.MUB6.Certificate.PairSemantics.raw4189step0 line 575
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical4189 line 577
  121. def OAI.MUB6.Certificate.PairSemantics.raw4190 line 586
  122. def OAI.MUB6.Certificate.PairSemantics.raw4190step0 line 588
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical4190 line 590
  124. def OAI.MUB6.Certificate.PairSemantics.raw4191 line 599
  125. def OAI.MUB6.Certificate.PairSemantics.raw4191step0 line 601
  126. def OAI.MUB6.Certificate.PairSemantics.raw4191step1 line 603
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical4191 line 605