OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical227.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7264 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw7264step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw7264step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7264 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw7265 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw7265step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw7265step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7265 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw7266 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw7266step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw7266step1 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7266 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw7267 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw7267step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw7267step1 line 81
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7267 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw7268 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw7268step0 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw7268step1 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7268 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw7269 line 115
  22. def OAI.MUB6.Certificate.PairSemantics.raw7269step0 line 117
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7269 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw7270 line 128
  25. def OAI.MUB6.Certificate.PairSemantics.raw7270step0 line 130
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7270 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw7271 line 141
  28. def OAI.MUB6.Certificate.PairSemantics.raw7271step0 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw7271step1 line 145
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7271 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw7272 line 160
  32. def OAI.MUB6.Certificate.PairSemantics.raw7272step0 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw7272step1 line 164
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7272 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw7273 line 179
  36. def OAI.MUB6.Certificate.PairSemantics.raw7273step0 line 181
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical7273 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw7274 line 192
  39. def OAI.MUB6.Certificate.PairSemantics.raw7274step0 line 194
  40. def OAI.MUB6.Certificate.PairSemantics.raw7274step1 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw7274step2 line 198
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7274 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw7275 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw7275step0 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw7275step1 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw7275step2 line 223
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical7275 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw7276 line 242
  49. def OAI.MUB6.Certificate.PairSemantics.raw7276step0 line 244
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7276 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw7277 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw7277step0 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical7277 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw7278 line 268
  55. def OAI.MUB6.Certificate.PairSemantics.raw7278step0 line 270
  56. def OAI.MUB6.Certificate.PairSemantics.raw7278step1 line 272
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7278 line 274
  58. def OAI.MUB6.Certificate.PairSemantics.raw7279 line 287
  59. def OAI.MUB6.Certificate.PairSemantics.raw7279step0 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw7279step1 line 291
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7279 line 293
  62. def OAI.MUB6.Certificate.PairSemantics.raw7280 line 306
  63. def OAI.MUB6.Certificate.PairSemantics.raw7280step0 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw7280step1 line 310
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7280 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw7281 line 325
  67. def OAI.MUB6.Certificate.PairSemantics.raw7281step0 line 327
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical7281 line 329
  69. def OAI.MUB6.Certificate.PairSemantics.raw7282 line 338
  70. def OAI.MUB6.Certificate.PairSemantics.raw7282step0 line 340
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7282 line 342
  72. def OAI.MUB6.Certificate.PairSemantics.raw7283 line 351
  73. def OAI.MUB6.Certificate.PairSemantics.raw7283step0 line 353
  74. def OAI.MUB6.Certificate.PairSemantics.raw7283step1 line 355
  75. def OAI.MUB6.Certificate.PairSemantics.raw7283step2 line 357
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7283 line 359
  77. def OAI.MUB6.Certificate.PairSemantics.raw7284 line 376
  78. def OAI.MUB6.Certificate.PairSemantics.raw7284step0 line 378
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical7284 line 380
  80. def OAI.MUB6.Certificate.PairSemantics.raw7285 line 389
  81. def OAI.MUB6.Certificate.PairSemantics.raw7285step0 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw7285step1 line 393
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7285 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw7286 line 408
  85. def OAI.MUB6.Certificate.PairSemantics.raw7286step0 line 410
  86. def OAI.MUB6.Certificate.PairSemantics.raw7286step1 line 412
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7286 line 414
  88. def OAI.MUB6.Certificate.PairSemantics.raw7287 line 427
  89. def OAI.MUB6.Certificate.PairSemantics.raw7287step0 line 429
  90. def OAI.MUB6.Certificate.PairSemantics.raw7287step1 line 431
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7287 line 433
  92. def OAI.MUB6.Certificate.PairSemantics.raw7288 line 446
  93. def OAI.MUB6.Certificate.PairSemantics.raw7288step0 line 448
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7288 line 450
  95. def OAI.MUB6.Certificate.PairSemantics.raw7289 line 459
  96. def OAI.MUB6.Certificate.PairSemantics.raw7289step0 line 461
  97. def OAI.MUB6.Certificate.PairSemantics.raw7289step1 line 463
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7289 line 465
  99. def OAI.MUB6.Certificate.PairSemantics.raw7290 line 478
  100. def OAI.MUB6.Certificate.PairSemantics.raw7290step0 line 480
  101. def OAI.MUB6.Certificate.PairSemantics.raw7290step1 line 482
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical7290 line 484
  103. def OAI.MUB6.Certificate.PairSemantics.raw7291 line 497
  104. def OAI.MUB6.Certificate.PairSemantics.raw7291step0 line 499
  105. def OAI.MUB6.Certificate.PairSemantics.raw7291step1 line 501
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical7291 line 503
  107. def OAI.MUB6.Certificate.PairSemantics.raw7292 line 516
  108. def OAI.MUB6.Certificate.PairSemantics.raw7292step0 line 518
  109. def OAI.MUB6.Certificate.PairSemantics.raw7292step1 line 520
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical7292 line 522
  111. def OAI.MUB6.Certificate.PairSemantics.raw7293 line 535
  112. def OAI.MUB6.Certificate.PairSemantics.raw7293step0 line 537
  113. def OAI.MUB6.Certificate.PairSemantics.raw7293step1 line 539
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical7293 line 541
  115. def OAI.MUB6.Certificate.PairSemantics.raw7294 line 554
  116. def OAI.MUB6.Certificate.PairSemantics.raw7294step0 line 556
  117. def OAI.MUB6.Certificate.PairSemantics.raw7294step1 line 558
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7294 line 560
  119. def OAI.MUB6.Certificate.PairSemantics.raw7295 line 573
  120. def OAI.MUB6.Certificate.PairSemantics.raw7295step0 line 575
  121. def OAI.MUB6.Certificate.PairSemantics.raw7295step1 line 577
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical7295 line 579