OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical285.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9120 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw9120step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9120 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw9121 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw9121step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9121 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw9122 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw9122step0 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9122 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw9123 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw9123step0 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9123 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw9124 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw9124step0 line 71
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9124 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw9125 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw9125step0 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw9125step1 line 86
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9125 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw9126 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw9126step0 line 104
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9126 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw9127 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw9127step0 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw9127step1 line 119
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9127 line 121
  27. def OAI.MUB6.Certificate.PairSemantics.raw9128 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw9128step0 line 136
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9128 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw9129 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw9129step0 line 149
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical9129 line 151
  33. def OAI.MUB6.Certificate.PairSemantics.raw9130 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw9130step0 line 162
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9130 line 164
  36. def OAI.MUB6.Certificate.PairSemantics.raw9131 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw9131step0 line 175
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9131 line 177
  39. def OAI.MUB6.Certificate.PairSemantics.raw9132 line 186
  40. def OAI.MUB6.Certificate.PairSemantics.raw9132step0 line 188
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9132 line 190
  42. def OAI.MUB6.Certificate.PairSemantics.raw9133 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw9133step0 line 201
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9133 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw9134 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw9134step0 line 214
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9134 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw9135 line 225
  49. def OAI.MUB6.Certificate.PairSemantics.raw9135step0 line 227
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9135 line 229
  51. def OAI.MUB6.Certificate.PairSemantics.raw9136 line 238
  52. def OAI.MUB6.Certificate.PairSemantics.raw9136step0 line 240
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9136 line 242
  54. def OAI.MUB6.Certificate.PairSemantics.raw9137 line 251
  55. def OAI.MUB6.Certificate.PairSemantics.raw9137step0 line 253
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9137 line 255
  57. def OAI.MUB6.Certificate.PairSemantics.raw9138 line 264
  58. def OAI.MUB6.Certificate.PairSemantics.raw9138step0 line 266
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9138 line 268
  60. def OAI.MUB6.Certificate.PairSemantics.raw9139 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw9139step0 line 279
  62. def OAI.MUB6.Certificate.PairSemantics.raw9139step1 line 281
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9139 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw9140 line 296
  65. def OAI.MUB6.Certificate.PairSemantics.raw9140step0 line 298
  66. def OAI.MUB6.Certificate.PairSemantics.raw9140step1 line 300
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9140 line 302
  68. def OAI.MUB6.Certificate.PairSemantics.raw9141 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw9141step0 line 317
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9141 line 319
  71. def OAI.MUB6.Certificate.PairSemantics.raw9142 line 328
  72. def OAI.MUB6.Certificate.PairSemantics.raw9142step0 line 330
  73. def OAI.MUB6.Certificate.PairSemantics.raw9142step1 line 332
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9142 line 334
  75. def OAI.MUB6.Certificate.PairSemantics.raw9143 line 347
  76. def OAI.MUB6.Certificate.PairSemantics.raw9143step0 line 349
  77. def OAI.MUB6.Certificate.PairSemantics.raw9143step1 line 351
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9143 line 353
  79. def OAI.MUB6.Certificate.PairSemantics.raw9144 line 366
  80. def OAI.MUB6.Certificate.PairSemantics.raw9144step0 line 368
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9144 line 370
  82. def OAI.MUB6.Certificate.PairSemantics.raw9145 line 379
  83. def OAI.MUB6.Certificate.PairSemantics.raw9145step0 line 381
  84. def OAI.MUB6.Certificate.PairSemantics.raw9145step1 line 383
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9145 line 385
  86. def OAI.MUB6.Certificate.PairSemantics.raw9146 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw9146step0 line 400
  88. def OAI.MUB6.Certificate.PairSemantics.raw9146step1 line 402
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9146 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw9147 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw9147step0 line 419
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9147 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw9148 line 430
  94. def OAI.MUB6.Certificate.PairSemantics.raw9148step0 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw9148step1 line 434
  96. def OAI.MUB6.Certificate.PairSemantics.raw9148step2 line 436
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9148 line 438
  98. def OAI.MUB6.Certificate.PairSemantics.raw9149 line 458
  99. def OAI.MUB6.Certificate.PairSemantics.raw9149step0 line 460
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9149 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw9150 line 471
  102. def OAI.MUB6.Certificate.PairSemantics.raw9150step0 line 473
  103. def OAI.MUB6.Certificate.PairSemantics.raw9150step1 line 475
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical9150 line 477
  105. def OAI.MUB6.Certificate.PairSemantics.raw9151 line 491
  106. def OAI.MUB6.Certificate.PairSemantics.raw9151step0 line 493
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9151 line 495