OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical8.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw256 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw256step0 line 15
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical256 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw257 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw257step0 line 28
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical257 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw258 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw258step0 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw258step1 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw258step2 line 45
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical258 line 47
  12. def OAI.MUB6.Certificate.PairSemantics.raw259 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw259step0 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw259step1 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw259step2 line 70
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical259 line 72
  17. def OAI.MUB6.Certificate.PairSemantics.raw260 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw260step0 line 91
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical260 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw261 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw261step0 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw261step1 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical261 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw262 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw262step0 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw262step1 line 125
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical262 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw263 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw263step0 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw263step1 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical263 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw264 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw264step0 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw264step1 line 163
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical264 line 165
  36. def OAI.MUB6.Certificate.PairSemantics.raw265 line 178
  37. def OAI.MUB6.Certificate.PairSemantics.raw265step0 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw265step1 line 182
  39. def OAI.MUB6.Certificate.PairSemantics.raw265step2 line 184
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical265 line 186
  41. def OAI.MUB6.Certificate.PairSemantics.raw266 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw266step0 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw266step1 line 207
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical266 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw267 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw267step0 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw267step1 line 226
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical267 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw268 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw268step0 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw268step1 line 245
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical268 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw269 line 260
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical269 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw270 line 266
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical270 line 268
  57. def OAI.MUB6.Certificate.PairSemantics.raw271 line 272
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical271 line 274
  59. def OAI.MUB6.Certificate.PairSemantics.raw272 line 278
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical272 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw273 line 284
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical273 line 286
  63. def OAI.MUB6.Certificate.PairSemantics.raw274 line 290
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical274 line 292
  65. def OAI.MUB6.Certificate.PairSemantics.raw275 line 296
  66. def OAI.MUB6.Certificate.PairSemantics.raw275step0 line 298
  67. def OAI.MUB6.Certificate.PairSemantics.raw275step1 line 300
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical275 line 302
  69. def OAI.MUB6.Certificate.PairSemantics.raw276 line 316
  70. def OAI.MUB6.Certificate.PairSemantics.raw276step0 line 318
  71. def OAI.MUB6.Certificate.PairSemantics.raw276step1 line 320
  72. def OAI.MUB6.Certificate.PairSemantics.raw276step2 line 322
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical276 line 324
  74. def OAI.MUB6.Certificate.PairSemantics.raw277 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw277step0 line 344
  76. def OAI.MUB6.Certificate.PairSemantics.raw277step1 line 346
  77. def OAI.MUB6.Certificate.PairSemantics.raw277step2 line 348
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical277 line 350
  79. def OAI.MUB6.Certificate.PairSemantics.raw278 line 368
  80. def OAI.MUB6.Certificate.PairSemantics.raw278step0 line 370
  81. def OAI.MUB6.Certificate.PairSemantics.raw278step1 line 372
  82. def OAI.MUB6.Certificate.PairSemantics.raw278step2 line 374
  83. def OAI.MUB6.Certificate.PairSemantics.raw278step3 line 376
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical278 line 378
  85. def OAI.MUB6.Certificate.PairSemantics.raw279 line 400
  86. def OAI.MUB6.Certificate.PairSemantics.raw279step0 line 402
  87. def OAI.MUB6.Certificate.PairSemantics.raw279step1 line 404
  88. def OAI.MUB6.Certificate.PairSemantics.raw279step2 line 406
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical279 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw280 line 426
  91. def OAI.MUB6.Certificate.PairSemantics.raw280step0 line 428
  92. def OAI.MUB6.Certificate.PairSemantics.raw280step1 line 430
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical280 line 432
  94. def OAI.MUB6.Certificate.PairSemantics.raw281 line 446
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical281 line 448
  96. def OAI.MUB6.Certificate.PairSemantics.raw282 line 452
  97. def OAI.MUB6.Certificate.PairSemantics.raw282step0 line 454
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical282 line 456
  99. def OAI.MUB6.Certificate.PairSemantics.raw283 line 465
  100. def OAI.MUB6.Certificate.PairSemantics.raw283step0 line 467
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical283 line 469
  102. def OAI.MUB6.Certificate.PairSemantics.raw284 line 478
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical284 line 480
  104. def OAI.MUB6.Certificate.PairSemantics.raw285 line 484
  105. def OAI.MUB6.Certificate.PairSemantics.raw285step0 line 486
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical285 line 488
  107. def OAI.MUB6.Certificate.PairSemantics.raw286 line 497
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical286 line 499
  109. def OAI.MUB6.Certificate.PairSemantics.raw287 line 503
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical287 line 505