OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical193.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6176 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw6176step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6176 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw6177 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw6177step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6177 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw6178 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw6178step0 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6178 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw6179 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6179 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw6180 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw6180step0 line 64
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6180 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw6181 line 75
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6181 line 77
  17. def OAI.MUB6.Certificate.PairSemantics.raw6182 line 81
  18. def OAI.MUB6.Certificate.PairSemantics.raw6182step0 line 83
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6182 line 85
  20. def OAI.MUB6.Certificate.PairSemantics.raw6183 line 94
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6183 line 96
  22. def OAI.MUB6.Certificate.PairSemantics.raw6184 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw6184step0 line 102
  24. def OAI.MUB6.Certificate.PairSemantics.raw6184step1 line 104
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6184 line 106
  26. def OAI.MUB6.Certificate.PairSemantics.raw6185 line 119
  27. def OAI.MUB6.Certificate.PairSemantics.raw6185step0 line 121
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6185 line 123
  29. def OAI.MUB6.Certificate.PairSemantics.raw6186 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw6186step0 line 134
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6186 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw6187 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw6187step0 line 147
  34. def OAI.MUB6.Certificate.PairSemantics.raw6187step1 line 149
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6187 line 151
  36. def OAI.MUB6.Certificate.PairSemantics.raw6188 line 164
  37. def OAI.MUB6.Certificate.PairSemantics.raw6188step0 line 166
  38. def OAI.MUB6.Certificate.PairSemantics.raw6188step1 line 168
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6188 line 170
  40. def OAI.MUB6.Certificate.PairSemantics.raw6189 line 183
  41. def OAI.MUB6.Certificate.PairSemantics.raw6189step0 line 185
  42. def OAI.MUB6.Certificate.PairSemantics.raw6189step1 line 187
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6189 line 189
  44. def OAI.MUB6.Certificate.PairSemantics.raw6190 line 202
  45. def OAI.MUB6.Certificate.PairSemantics.raw6190step0 line 204
  46. def OAI.MUB6.Certificate.PairSemantics.raw6190step1 line 206
  47. def OAI.MUB6.Certificate.PairSemantics.raw6190step2 line 208
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6190 line 210
  49. def OAI.MUB6.Certificate.PairSemantics.raw6191 line 227
  50. def OAI.MUB6.Certificate.PairSemantics.raw6191step0 line 229
  51. def OAI.MUB6.Certificate.PairSemantics.raw6191step1 line 231
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6191 line 233
  53. def OAI.MUB6.Certificate.PairSemantics.raw6192 line 246
  54. def OAI.MUB6.Certificate.PairSemantics.raw6192step0 line 248
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6192 line 250
  56. def OAI.MUB6.Certificate.PairSemantics.raw6193 line 259
  57. def OAI.MUB6.Certificate.PairSemantics.raw6193step0 line 261
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6193 line 263
  59. def OAI.MUB6.Certificate.PairSemantics.raw6194 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw6194step0 line 274
  61. def OAI.MUB6.Certificate.PairSemantics.raw6194step1 line 276
  62. def OAI.MUB6.Certificate.PairSemantics.raw6194step2 line 278
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6194 line 280
  64. def OAI.MUB6.Certificate.PairSemantics.raw6195 line 297
  65. def OAI.MUB6.Certificate.PairSemantics.raw6195step0 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw6195step1 line 301
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6195 line 303
  68. def OAI.MUB6.Certificate.PairSemantics.raw6196 line 316
  69. def OAI.MUB6.Certificate.PairSemantics.raw6196step0 line 318
  70. def OAI.MUB6.Certificate.PairSemantics.raw6196step1 line 320
  71. def OAI.MUB6.Certificate.PairSemantics.raw6196step2 line 322
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6196 line 324
  73. def OAI.MUB6.Certificate.PairSemantics.raw6197 line 341
  74. def OAI.MUB6.Certificate.PairSemantics.raw6197step0 line 343
  75. def OAI.MUB6.Certificate.PairSemantics.raw6197step1 line 345
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6197 line 347
  77. def OAI.MUB6.Certificate.PairSemantics.raw6198 line 360
  78. def OAI.MUB6.Certificate.PairSemantics.raw6198step0 line 362
  79. def OAI.MUB6.Certificate.PairSemantics.raw6198step1 line 364
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6198 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw6199 line 379
  82. def OAI.MUB6.Certificate.PairSemantics.raw6199step0 line 381
  83. def OAI.MUB6.Certificate.PairSemantics.raw6199step1 line 383
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6199 line 385
  85. def OAI.MUB6.Certificate.PairSemantics.raw6200 line 398
  86. def OAI.MUB6.Certificate.PairSemantics.raw6200step0 line 400
  87. def OAI.MUB6.Certificate.PairSemantics.raw6200step1 line 402
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6200 line 404
  89. def OAI.MUB6.Certificate.PairSemantics.raw6201 line 417
  90. def OAI.MUB6.Certificate.PairSemantics.raw6201step0 line 419
  91. def OAI.MUB6.Certificate.PairSemantics.raw6201step1 line 421
  92. def OAI.MUB6.Certificate.PairSemantics.raw6201step2 line 423
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6201 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw6202 line 442
  95. def OAI.MUB6.Certificate.PairSemantics.raw6202step0 line 444
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical6202 line 446
  97. def OAI.MUB6.Certificate.PairSemantics.raw6203 line 455
  98. def OAI.MUB6.Certificate.PairSemantics.raw6203step0 line 457
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6203 line 459
  100. def OAI.MUB6.Certificate.PairSemantics.raw6204 line 468
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical6204 line 470
  102. def OAI.MUB6.Certificate.PairSemantics.raw6205 line 474
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6205 line 476
  104. def OAI.MUB6.Certificate.PairSemantics.raw6206 line 480
  105. def OAI.MUB6.Certificate.PairSemantics.raw6206step0 line 482
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical6206 line 484
  107. def OAI.MUB6.Certificate.PairSemantics.raw6207 line 493
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6207 line 495