OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical5.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw160 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw160step0 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw160step1 line 16
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical160 line 18
  5. def OAI.MUB6.Certificate.PairSemantics.raw161 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw161step0 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw161step1 line 35
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical161 line 37
  9. def OAI.MUB6.Certificate.PairSemantics.raw162 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw162step0 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw162step1 line 54
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical162 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw163 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw163step0 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw163step1 line 73
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical163 line 75
  17. def OAI.MUB6.Certificate.PairSemantics.raw164 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw164step0 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw164step1 line 92
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical164 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw165 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw165step0 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw165step1 line 111
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical165 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw166 line 126
  26. def OAI.MUB6.Certificate.PairSemantics.raw166step0 line 128
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical166 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw167 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw167step0 line 141
  30. def OAI.MUB6.Certificate.PairSemantics.raw167step1 line 143
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical167 line 145
  32. def OAI.MUB6.Certificate.PairSemantics.raw168 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw168step0 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw168step1 line 162
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical168 line 164
  36. def OAI.MUB6.Certificate.PairSemantics.raw169 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw169step0 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw169step1 line 181
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical169 line 183
  40. def OAI.MUB6.Certificate.PairSemantics.raw170 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw170step0 line 198
  42. def OAI.MUB6.Certificate.PairSemantics.raw170step1 line 200
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical170 line 202
  44. def OAI.MUB6.Certificate.PairSemantics.raw171 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw171step0 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw171step1 line 219
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical171 line 221
  48. def OAI.MUB6.Certificate.PairSemantics.raw172 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw172step0 line 236
  50. def OAI.MUB6.Certificate.PairSemantics.raw172step1 line 238
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical172 line 240
  52. def OAI.MUB6.Certificate.PairSemantics.raw173 line 253
  53. def OAI.MUB6.Certificate.PairSemantics.raw173step0 line 255
  54. def OAI.MUB6.Certificate.PairSemantics.raw173step1 line 257
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical173 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw174 line 272
  57. def OAI.MUB6.Certificate.PairSemantics.raw174step0 line 274
  58. def OAI.MUB6.Certificate.PairSemantics.raw174step1 line 276
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical174 line 278
  60. def OAI.MUB6.Certificate.PairSemantics.raw175 line 291
  61. def OAI.MUB6.Certificate.PairSemantics.raw175step0 line 293
  62. def OAI.MUB6.Certificate.PairSemantics.raw175step1 line 295
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical175 line 297
  64. def OAI.MUB6.Certificate.PairSemantics.raw176 line 310
  65. def OAI.MUB6.Certificate.PairSemantics.raw176step0 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw176step1 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw176step2 line 316
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical176 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw177 line 335
  70. def OAI.MUB6.Certificate.PairSemantics.raw177step0 line 337
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical177 line 339
  72. def OAI.MUB6.Certificate.PairSemantics.raw178 line 348
  73. def OAI.MUB6.Certificate.PairSemantics.raw178step0 line 350
  74. def OAI.MUB6.Certificate.PairSemantics.raw178step1 line 352
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical178 line 354
  76. def OAI.MUB6.Certificate.PairSemantics.raw179 line 367
  77. def OAI.MUB6.Certificate.PairSemantics.raw179step0 line 369
  78. def OAI.MUB6.Certificate.PairSemantics.raw179step1 line 371
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical179 line 373
  80. def OAI.MUB6.Certificate.PairSemantics.raw180 line 386
  81. def OAI.MUB6.Certificate.PairSemantics.raw180step0 line 388
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical180 line 390
  83. def OAI.MUB6.Certificate.PairSemantics.raw181 line 399
  84. def OAI.MUB6.Certificate.PairSemantics.raw181step0 line 401
  85. def OAI.MUB6.Certificate.PairSemantics.raw181step1 line 403
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical181 line 405
  87. def OAI.MUB6.Certificate.PairSemantics.raw182 line 418
  88. def OAI.MUB6.Certificate.PairSemantics.raw182step0 line 420
  89. def OAI.MUB6.Certificate.PairSemantics.raw182step1 line 422
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical182 line 424
  91. def OAI.MUB6.Certificate.PairSemantics.raw183 line 437
  92. def OAI.MUB6.Certificate.PairSemantics.raw183step0 line 439
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical183 line 441
  94. def OAI.MUB6.Certificate.PairSemantics.raw184 line 451
  95. def OAI.MUB6.Certificate.PairSemantics.raw184step0 line 453
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical184 line 455
  97. def OAI.MUB6.Certificate.PairSemantics.raw185 line 465
  98. def OAI.MUB6.Certificate.PairSemantics.raw185step0 line 467
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical185 line 469
  100. def OAI.MUB6.Certificate.PairSemantics.raw186 line 479
  101. def OAI.MUB6.Certificate.PairSemantics.raw186step0 line 481
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical186 line 483
  103. def OAI.MUB6.Certificate.PairSemantics.raw187 line 493
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical187 line 495
  105. def OAI.MUB6.Certificate.PairSemantics.raw188 line 499
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical188 line 501
  107. def OAI.MUB6.Certificate.PairSemantics.raw189 line 505
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical189 line 507
  109. def OAI.MUB6.Certificate.PairSemantics.raw190 line 511
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical190 line 513
  111. def OAI.MUB6.Certificate.PairSemantics.raw191 line 517
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical191 line 519