OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical65.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2080 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw2080step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw2080step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2080 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw2081 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw2081step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw2081step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2081 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw2082 line 54
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2082 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw2083 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw2083step0 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw2083step1 line 64
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical2083 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw2084 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw2084step0 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw2084step1 line 83
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2084 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw2085 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw2085step0 line 100
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2085 line 102
  22. def OAI.MUB6.Certificate.PairSemantics.raw2086 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw2086step0 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw2086step1 line 115
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2086 line 117
  26. def OAI.MUB6.Certificate.PairSemantics.raw2087 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2087 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw2088 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw2088step0 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw2088step1 line 140
  31. def OAI.MUB6.Certificate.PairSemantics.raw2088step2 line 142
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2088 line 144
  33. def OAI.MUB6.Certificate.PairSemantics.raw2089 line 161
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2089 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw2090 line 167
  36. def OAI.MUB6.Certificate.PairSemantics.raw2090step0 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw2090step1 line 171
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical2090 line 173
  39. def OAI.MUB6.Certificate.PairSemantics.raw2091 line 186
  40. def OAI.MUB6.Certificate.PairSemantics.raw2091step0 line 188
  41. def OAI.MUB6.Certificate.PairSemantics.raw2091step1 line 190
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2091 line 192
  43. def OAI.MUB6.Certificate.PairSemantics.raw2092 line 205
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2092 line 207
  45. def OAI.MUB6.Certificate.PairSemantics.raw2093 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw2093step0 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw2093step1 line 215
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2093 line 217
  49. def OAI.MUB6.Certificate.PairSemantics.raw2094 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw2094step0 line 232
  51. def OAI.MUB6.Certificate.PairSemantics.raw2094step1 line 234
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2094 line 236
  53. def OAI.MUB6.Certificate.PairSemantics.raw2095 line 249
  54. def OAI.MUB6.Certificate.PairSemantics.raw2095step0 line 251
  55. def OAI.MUB6.Certificate.PairSemantics.raw2095step1 line 253
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2095 line 255
  57. def OAI.MUB6.Certificate.PairSemantics.raw2096 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw2096step0 line 270
  59. def OAI.MUB6.Certificate.PairSemantics.raw2096step1 line 272
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2096 line 274
  61. def OAI.MUB6.Certificate.PairSemantics.raw2097 line 287
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2097 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw2098 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw2098step0 line 295
  65. def OAI.MUB6.Certificate.PairSemantics.raw2098step1 line 297
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2098 line 299
  67. def OAI.MUB6.Certificate.PairSemantics.raw2099 line 312
  68. def OAI.MUB6.Certificate.PairSemantics.raw2099step0 line 314
  69. def OAI.MUB6.Certificate.PairSemantics.raw2099step1 line 316
  70. def OAI.MUB6.Certificate.PairSemantics.raw2099step2 line 318
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2099 line 320
  72. def OAI.MUB6.Certificate.PairSemantics.raw2100 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw2100step0 line 339
  74. def OAI.MUB6.Certificate.PairSemantics.raw2100step1 line 341
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2100 line 343
  76. def OAI.MUB6.Certificate.PairSemantics.raw2101 line 356
  77. def OAI.MUB6.Certificate.PairSemantics.raw2101step0 line 358
  78. def OAI.MUB6.Certificate.PairSemantics.raw2101step1 line 360
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2101 line 362
  80. def OAI.MUB6.Certificate.PairSemantics.raw2102 line 375
  81. def OAI.MUB6.Certificate.PairSemantics.raw2102step0 line 377
  82. def OAI.MUB6.Certificate.PairSemantics.raw2102step1 line 379
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2102 line 381
  84. def OAI.MUB6.Certificate.PairSemantics.raw2103 line 394
  85. def OAI.MUB6.Certificate.PairSemantics.raw2103step0 line 396
  86. def OAI.MUB6.Certificate.PairSemantics.raw2103step1 line 398
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2103 line 400
  88. def OAI.MUB6.Certificate.PairSemantics.raw2104 line 413
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2104 line 415
  90. def OAI.MUB6.Certificate.PairSemantics.raw2105 line 419
  91. def OAI.MUB6.Certificate.PairSemantics.raw2105step0 line 421
  92. def OAI.MUB6.Certificate.PairSemantics.raw2105step1 line 423
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical2105 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw2106 line 438
  95. def OAI.MUB6.Certificate.PairSemantics.raw2106step0 line 440
  96. def OAI.MUB6.Certificate.PairSemantics.raw2106step1 line 442
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2106 line 444
  98. def OAI.MUB6.Certificate.PairSemantics.raw2107 line 457
  99. def OAI.MUB6.Certificate.PairSemantics.raw2107step0 line 459
  100. def OAI.MUB6.Certificate.PairSemantics.raw2107step1 line 461
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical2107 line 463
  102. def OAI.MUB6.Certificate.PairSemantics.raw2108 line 476
  103. def OAI.MUB6.Certificate.PairSemantics.raw2108step0 line 478
  104. def OAI.MUB6.Certificate.PairSemantics.raw2108step1 line 480
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical2108 line 482
  106. def OAI.MUB6.Certificate.PairSemantics.raw2109 line 495
  107. def OAI.MUB6.Certificate.PairSemantics.raw2109step0 line 497
  108. def OAI.MUB6.Certificate.PairSemantics.raw2109step1 line 499
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical2109 line 501
  110. def OAI.MUB6.Certificate.PairSemantics.raw2110 line 514
  111. def OAI.MUB6.Certificate.PairSemantics.raw2110step0 line 516
  112. def OAI.MUB6.Certificate.PairSemantics.raw2110step1 line 518
  113. def OAI.MUB6.Certificate.PairSemantics.raw2110step2 line 520
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical2110 line 522
  115. def OAI.MUB6.Certificate.PairSemantics.raw2111 line 539
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical2111 line 541