OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical66.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2112 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw2112step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw2112step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2112 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw2113 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw2113step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw2113step1 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw2113step2 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2113 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw2114 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw2114step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw2114step1 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2114 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw2115 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw2115step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw2115step1 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw2115step2 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2115 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw2116 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw2116step0 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw2116step1 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2116 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw2117 line 126
  24. def OAI.MUB6.Certificate.PairSemantics.raw2117step0 line 128
  25. def OAI.MUB6.Certificate.PairSemantics.raw2117step1 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw2117step2 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2117 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw2118 line 151
  29. def OAI.MUB6.Certificate.PairSemantics.raw2118step0 line 153
  30. def OAI.MUB6.Certificate.PairSemantics.raw2118step1 line 155
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2118 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw2119 line 170
  33. def OAI.MUB6.Certificate.PairSemantics.raw2119step0 line 172
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2119 line 174
  35. def OAI.MUB6.Certificate.PairSemantics.raw2120 line 183
  36. def OAI.MUB6.Certificate.PairSemantics.raw2120step0 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw2120step1 line 187
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical2120 line 189
  39. def OAI.MUB6.Certificate.PairSemantics.raw2121 line 202
  40. def OAI.MUB6.Certificate.PairSemantics.raw2121step0 line 204
  41. def OAI.MUB6.Certificate.PairSemantics.raw2121step1 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw2121step2 line 208
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2121 line 210
  44. def OAI.MUB6.Certificate.PairSemantics.raw2122 line 227
  45. def OAI.MUB6.Certificate.PairSemantics.raw2122step0 line 229
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2122 line 231
  47. def OAI.MUB6.Certificate.PairSemantics.raw2123 line 240
  48. def OAI.MUB6.Certificate.PairSemantics.raw2123step0 line 242
  49. def OAI.MUB6.Certificate.PairSemantics.raw2123step1 line 244
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical2123 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw2124 line 259
  52. def OAI.MUB6.Certificate.PairSemantics.raw2124step0 line 261
  53. def OAI.MUB6.Certificate.PairSemantics.raw2124step1 line 263
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2124 line 265
  55. def OAI.MUB6.Certificate.PairSemantics.raw2125 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw2125step0 line 280
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2125 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw2126 line 291
  59. def OAI.MUB6.Certificate.PairSemantics.raw2126step0 line 293
  60. def OAI.MUB6.Certificate.PairSemantics.raw2126step1 line 295
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2126 line 297
  62. def OAI.MUB6.Certificate.PairSemantics.raw2127 line 310
  63. def OAI.MUB6.Certificate.PairSemantics.raw2127step0 line 312
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2127 line 314
  65. def OAI.MUB6.Certificate.PairSemantics.raw2128 line 323
  66. def OAI.MUB6.Certificate.PairSemantics.raw2128step0 line 325
  67. def OAI.MUB6.Certificate.PairSemantics.raw2128step1 line 327
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical2128 line 329
  69. def OAI.MUB6.Certificate.PairSemantics.raw2129 line 342
  70. def OAI.MUB6.Certificate.PairSemantics.raw2129step0 line 344
  71. def OAI.MUB6.Certificate.PairSemantics.raw2129step1 line 346
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2129 line 348
  73. def OAI.MUB6.Certificate.PairSemantics.raw2130 line 361
  74. def OAI.MUB6.Certificate.PairSemantics.raw2130step0 line 363
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2130 line 365
  76. def OAI.MUB6.Certificate.PairSemantics.raw2131 line 374
  77. def OAI.MUB6.Certificate.PairSemantics.raw2131step0 line 376
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2131 line 378
  79. def OAI.MUB6.Certificate.PairSemantics.raw2132 line 387
  80. def OAI.MUB6.Certificate.PairSemantics.raw2132step0 line 389
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical2132 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw2133 line 400
  83. def OAI.MUB6.Certificate.PairSemantics.raw2133step0 line 402
  84. def OAI.MUB6.Certificate.PairSemantics.raw2133step1 line 404
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical2133 line 406
  86. def OAI.MUB6.Certificate.PairSemantics.raw2134 line 419
  87. def OAI.MUB6.Certificate.PairSemantics.raw2134step0 line 421
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2134 line 423
  89. def OAI.MUB6.Certificate.PairSemantics.raw2135 line 432
  90. def OAI.MUB6.Certificate.PairSemantics.raw2135step0 line 434
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical2135 line 436
  92. def OAI.MUB6.Certificate.PairSemantics.raw2136 line 445
  93. def OAI.MUB6.Certificate.PairSemantics.raw2136step0 line 447
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2136 line 449
  95. def OAI.MUB6.Certificate.PairSemantics.raw2137 line 458
  96. def OAI.MUB6.Certificate.PairSemantics.raw2137step0 line 460
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2137 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw2138 line 471
  99. def OAI.MUB6.Certificate.PairSemantics.raw2138step0 line 473
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical2138 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw2139 line 484
  102. def OAI.MUB6.Certificate.PairSemantics.raw2139step0 line 486
  103. def OAI.MUB6.Certificate.PairSemantics.raw2139step1 line 488
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical2139 line 490
  105. def OAI.MUB6.Certificate.PairSemantics.raw2140 line 503
  106. def OAI.MUB6.Certificate.PairSemantics.raw2140step0 line 505
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical2140 line 507
  108. def OAI.MUB6.Certificate.PairSemantics.raw2141 line 516
  109. def OAI.MUB6.Certificate.PairSemantics.raw2141step0 line 518
  110. def OAI.MUB6.Certificate.PairSemantics.raw2141step1 line 520
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical2141 line 522
  112. def OAI.MUB6.Certificate.PairSemantics.raw2142 line 535
  113. def OAI.MUB6.Certificate.PairSemantics.raw2142step0 line 537
  114. def OAI.MUB6.Certificate.PairSemantics.raw2142step1 line 539
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical2142 line 541
  116. def OAI.MUB6.Certificate.PairSemantics.raw2143 line 554
  117. def OAI.MUB6.Certificate.PairSemantics.raw2143step0 line 556
  118. def OAI.MUB6.Certificate.PairSemantics.raw2143step1 line 558
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical2143 line 560