OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical315.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw10080 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw10080step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical10080 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw10081 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw10081step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical10081 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw10082 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw10082step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical10082 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw10083 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw10083step0 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical10083 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw10084 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw10084step0 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical10084 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw10085 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw10085step0 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical10085 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw10086 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw10086step0 line 95
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical10086 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw10087 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw10087step0 line 108
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical10087 line 110
  25. def OAI.MUB6.Certificate.PairSemantics.raw10088 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw10088step0 line 121
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical10088 line 123
  28. def OAI.MUB6.Certificate.PairSemantics.raw10089 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw10089step0 line 134
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical10089 line 136
  31. def OAI.MUB6.Certificate.PairSemantics.raw10090 line 145
  32. def OAI.MUB6.Certificate.PairSemantics.raw10090step0 line 147
  33. def OAI.MUB6.Certificate.PairSemantics.raw10090step1 line 149
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical10090 line 151
  35. def OAI.MUB6.Certificate.PairSemantics.raw10091 line 164
  36. def OAI.MUB6.Certificate.PairSemantics.raw10091step0 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw10091step1 line 168
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical10091 line 170
  39. def OAI.MUB6.Certificate.PairSemantics.raw10092 line 183
  40. def OAI.MUB6.Certificate.PairSemantics.raw10092step0 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw10092step1 line 187
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical10092 line 189
  43. def OAI.MUB6.Certificate.PairSemantics.raw10093 line 202
  44. def OAI.MUB6.Certificate.PairSemantics.raw10093step0 line 204
  45. def OAI.MUB6.Certificate.PairSemantics.raw10093step1 line 206
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical10093 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw10094 line 221
  48. def OAI.MUB6.Certificate.PairSemantics.raw10094step0 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw10094step1 line 225
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical10094 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw10095 line 240
  52. def OAI.MUB6.Certificate.PairSemantics.raw10095step0 line 242
  53. def OAI.MUB6.Certificate.PairSemantics.raw10095step1 line 244
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical10095 line 246
  55. def OAI.MUB6.Certificate.PairSemantics.raw10096 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw10096step0 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw10096step1 line 263
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical10096 line 265
  59. def OAI.MUB6.Certificate.PairSemantics.raw10097 line 278
  60. def OAI.MUB6.Certificate.PairSemantics.raw10097step0 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw10097step1 line 282
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical10097 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw10098 line 297
  64. def OAI.MUB6.Certificate.PairSemantics.raw10098step0 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw10098step1 line 301
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical10098 line 303
  67. def OAI.MUB6.Certificate.PairSemantics.raw10099 line 316
  68. def OAI.MUB6.Certificate.PairSemantics.raw10099step0 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw10099step1 line 320
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical10099 line 322
  71. def OAI.MUB6.Certificate.PairSemantics.raw10100 line 335
  72. def OAI.MUB6.Certificate.PairSemantics.raw10100step0 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw10100step1 line 339
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical10100 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw10101 line 354
  76. def OAI.MUB6.Certificate.PairSemantics.raw10101step0 line 356
  77. def OAI.MUB6.Certificate.PairSemantics.raw10101step1 line 358
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical10101 line 360
  79. def OAI.MUB6.Certificate.PairSemantics.raw10102 line 373
  80. def OAI.MUB6.Certificate.PairSemantics.raw10102step0 line 375
  81. def OAI.MUB6.Certificate.PairSemantics.raw10102step1 line 377
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical10102 line 379
  83. def OAI.MUB6.Certificate.PairSemantics.raw10103 line 392
  84. def OAI.MUB6.Certificate.PairSemantics.raw10103step0 line 394
  85. def OAI.MUB6.Certificate.PairSemantics.raw10103step1 line 396
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical10103 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw10104 line 411
  88. def OAI.MUB6.Certificate.PairSemantics.raw10104step0 line 413
  89. def OAI.MUB6.Certificate.PairSemantics.raw10104step1 line 415
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical10104 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw10105 line 430
  92. def OAI.MUB6.Certificate.PairSemantics.raw10105step0 line 432
  93. def OAI.MUB6.Certificate.PairSemantics.raw10105step1 line 434
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical10105 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw10106 line 449
  96. def OAI.MUB6.Certificate.PairSemantics.raw10106step0 line 451
  97. def OAI.MUB6.Certificate.PairSemantics.raw10106step1 line 453
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical10106 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw10107 line 468
  100. def OAI.MUB6.Certificate.PairSemantics.raw10107step0 line 470
  101. def OAI.MUB6.Certificate.PairSemantics.raw10107step1 line 472
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical10107 line 474
  103. def OAI.MUB6.Certificate.PairSemantics.raw10108 line 487
  104. def OAI.MUB6.Certificate.PairSemantics.raw10108step0 line 489
  105. def OAI.MUB6.Certificate.PairSemantics.raw10108step1 line 491
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical10108 line 493
  107. def OAI.MUB6.Certificate.PairSemantics.raw10109 line 506
  108. def OAI.MUB6.Certificate.PairSemantics.raw10109step0 line 508
  109. def OAI.MUB6.Certificate.PairSemantics.raw10109step1 line 510
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical10109 line 512
  111. def OAI.MUB6.Certificate.PairSemantics.raw10110 line 525
  112. def OAI.MUB6.Certificate.PairSemantics.raw10110step0 line 527
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical10110 line 529
  114. def OAI.MUB6.Certificate.PairSemantics.raw10111 line 538
  115. def OAI.MUB6.Certificate.PairSemantics.raw10111step0 line 540
  116. def OAI.MUB6.Certificate.PairSemantics.raw10111step1 line 542
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical10111 line 544