OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical3.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw96 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw96step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw96step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical96 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw97 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw97step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw97step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical97 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw98 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw98step0 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw98step1 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical98 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw99 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw99step0 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw99step1 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical99 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw100 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw100step0 line 94
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical100 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw101 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw101step0 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw101step1 line 109
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical101 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw102 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw102step0 line 126
  26. def OAI.MUB6.Certificate.PairSemantics.raw102step1 line 128
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical102 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw103 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw103step0 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw103step1 line 147
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical103 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw104 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw104step0 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw104step1 line 166
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical104 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw105 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw105step0 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw105step1 line 185
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical105 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw106 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw106step0 line 202
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical106 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw107 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw107step0 line 215
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical107 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw108 line 226
  47. def OAI.MUB6.Certificate.PairSemantics.raw108step0 line 228
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical108 line 230
  49. def OAI.MUB6.Certificate.PairSemantics.raw109 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw109step0 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw109step1 line 243
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical109 line 245
  53. def OAI.MUB6.Certificate.PairSemantics.raw110 line 258
  54. def OAI.MUB6.Certificate.PairSemantics.raw110step0 line 260
  55. def OAI.MUB6.Certificate.PairSemantics.raw110step1 line 262
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical110 line 264
  57. def OAI.MUB6.Certificate.PairSemantics.raw111 line 277
  58. def OAI.MUB6.Certificate.PairSemantics.raw111step0 line 279
  59. def OAI.MUB6.Certificate.PairSemantics.raw111step1 line 281
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical111 line 283
  61. def OAI.MUB6.Certificate.PairSemantics.raw112 line 296
  62. def OAI.MUB6.Certificate.PairSemantics.raw112step0 line 298
  63. def OAI.MUB6.Certificate.PairSemantics.raw112step1 line 300
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical112 line 302
  65. def OAI.MUB6.Certificate.PairSemantics.raw113 line 315
  66. def OAI.MUB6.Certificate.PairSemantics.raw113step0 line 317
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical113 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw114 line 328
  69. def OAI.MUB6.Certificate.PairSemantics.raw114step0 line 330
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical114 line 332
  71. def OAI.MUB6.Certificate.PairSemantics.raw115 line 341
  72. def OAI.MUB6.Certificate.PairSemantics.raw115step0 line 343
  73. def OAI.MUB6.Certificate.PairSemantics.raw115step1 line 345
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical115 line 347
  75. def OAI.MUB6.Certificate.PairSemantics.raw116 line 360
  76. def OAI.MUB6.Certificate.PairSemantics.raw116step0 line 362
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical116 line 364
  78. def OAI.MUB6.Certificate.PairSemantics.raw117 line 373
  79. def OAI.MUB6.Certificate.PairSemantics.raw117step0 line 375
  80. def OAI.MUB6.Certificate.PairSemantics.raw117step1 line 377
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical117 line 379
  82. def OAI.MUB6.Certificate.PairSemantics.raw118 line 392
  83. def OAI.MUB6.Certificate.PairSemantics.raw118step0 line 394
  84. def OAI.MUB6.Certificate.PairSemantics.raw118step1 line 396
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical118 line 398
  86. def OAI.MUB6.Certificate.PairSemantics.raw119 line 411
  87. def OAI.MUB6.Certificate.PairSemantics.raw119step0 line 413
  88. def OAI.MUB6.Certificate.PairSemantics.raw119step1 line 415
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical119 line 417
  90. def OAI.MUB6.Certificate.PairSemantics.raw120 line 430
  91. def OAI.MUB6.Certificate.PairSemantics.raw120step0 line 432
  92. def OAI.MUB6.Certificate.PairSemantics.raw120step1 line 434
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical120 line 436
  94. def OAI.MUB6.Certificate.PairSemantics.raw121 line 449
  95. def OAI.MUB6.Certificate.PairSemantics.raw121step0 line 451
  96. def OAI.MUB6.Certificate.PairSemantics.raw121step1 line 453
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical121 line 455
  98. def OAI.MUB6.Certificate.PairSemantics.raw122 line 468
  99. def OAI.MUB6.Certificate.PairSemantics.raw122step0 line 470
  100. def OAI.MUB6.Certificate.PairSemantics.raw122step1 line 472
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical122 line 474
  102. def OAI.MUB6.Certificate.PairSemantics.raw123 line 487
  103. def OAI.MUB6.Certificate.PairSemantics.raw123step0 line 489
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical123 line 491
  105. def OAI.MUB6.Certificate.PairSemantics.raw124 line 500
  106. def OAI.MUB6.Certificate.PairSemantics.raw124step0 line 502
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical124 line 504
  108. def OAI.MUB6.Certificate.PairSemantics.raw125 line 513
  109. def OAI.MUB6.Certificate.PairSemantics.raw125step0 line 515
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical125 line 517
  111. def OAI.MUB6.Certificate.PairSemantics.raw126 line 526
  112. def OAI.MUB6.Certificate.PairSemantics.raw126step0 line 528
  113. def OAI.MUB6.Certificate.PairSemantics.raw126step1 line 530
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical126 line 532
  115. def OAI.MUB6.Certificate.PairSemantics.raw127 line 545
  116. def OAI.MUB6.Certificate.PairSemantics.raw127step0 line 547
  117. def OAI.MUB6.Certificate.PairSemantics.raw127step1 line 549
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical127 line 551