OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical313.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw10016 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw10016step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical10016 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw10017 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw10017step0 line 33
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical10017 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw10018 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw10018step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical10018 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw10019 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw10019step0 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical10019 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw10020 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw10020step0 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw10020step1 line 74
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical10020 line 76
  17. def OAI.MUB6.Certificate.PairSemantics.raw10021 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw10021step0 line 92
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical10021 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw10022 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw10022step0 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical10022 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw10023 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw10023step0 line 118
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical10023 line 120
  26. def OAI.MUB6.Certificate.PairSemantics.raw10024 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw10024step0 line 131
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical10024 line 133
  29. def OAI.MUB6.Certificate.PairSemantics.raw10025 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw10025step0 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical10025 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw10026 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw10026step0 line 157
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical10026 line 159
  35. def OAI.MUB6.Certificate.PairSemantics.raw10027 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw10027step0 line 170
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical10027 line 172
  38. def OAI.MUB6.Certificate.PairSemantics.raw10028 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw10028step0 line 183
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical10028 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw10029 line 194
  42. def OAI.MUB6.Certificate.PairSemantics.raw10029step0 line 196
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical10029 line 198
  44. def OAI.MUB6.Certificate.PairSemantics.raw10030 line 207
  45. def OAI.MUB6.Certificate.PairSemantics.raw10030step0 line 209
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical10030 line 211
  47. def OAI.MUB6.Certificate.PairSemantics.raw10031 line 220
  48. def OAI.MUB6.Certificate.PairSemantics.raw10031step0 line 222
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical10031 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw10032 line 233
  51. def OAI.MUB6.Certificate.PairSemantics.raw10032step0 line 235
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical10032 line 237
  53. def OAI.MUB6.Certificate.PairSemantics.raw10033 line 246
  54. def OAI.MUB6.Certificate.PairSemantics.raw10033step0 line 248
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical10033 line 250
  56. def OAI.MUB6.Certificate.PairSemantics.raw10034 line 259
  57. def OAI.MUB6.Certificate.PairSemantics.raw10034step0 line 261
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical10034 line 263
  59. def OAI.MUB6.Certificate.PairSemantics.raw10035 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw10035step0 line 274
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical10035 line 276
  62. def OAI.MUB6.Certificate.PairSemantics.raw10036 line 285
  63. def OAI.MUB6.Certificate.PairSemantics.raw10036step0 line 287
  64. def OAI.MUB6.Certificate.PairSemantics.raw10036step1 line 289
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical10036 line 291
  66. def OAI.MUB6.Certificate.PairSemantics.raw10037 line 304
  67. def OAI.MUB6.Certificate.PairSemantics.raw10037step0 line 306
  68. def OAI.MUB6.Certificate.PairSemantics.raw10037step1 line 308
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical10037 line 310
  70. def OAI.MUB6.Certificate.PairSemantics.raw10038 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw10038step0 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical10038 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw10039 line 336
  74. def OAI.MUB6.Certificate.PairSemantics.raw10039step0 line 338
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical10039 line 340
  76. def OAI.MUB6.Certificate.PairSemantics.raw10040 line 349
  77. def OAI.MUB6.Certificate.PairSemantics.raw10040step0 line 351
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical10040 line 353
  79. def OAI.MUB6.Certificate.PairSemantics.raw10041 line 362
  80. def OAI.MUB6.Certificate.PairSemantics.raw10041step0 line 364
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical10041 line 366
  82. def OAI.MUB6.Certificate.PairSemantics.raw10042 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw10042step0 line 377
  84. def OAI.MUB6.Certificate.PairSemantics.raw10042step1 line 379
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical10042 line 381
  86. def OAI.MUB6.Certificate.PairSemantics.raw10043 line 394
  87. def OAI.MUB6.Certificate.PairSemantics.raw10043step0 line 396
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical10043 line 398
  89. def OAI.MUB6.Certificate.PairSemantics.raw10044 line 407
  90. def OAI.MUB6.Certificate.PairSemantics.raw10044step0 line 409
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical10044 line 411
  92. def OAI.MUB6.Certificate.PairSemantics.raw10045 line 420
  93. def OAI.MUB6.Certificate.PairSemantics.raw10045step0 line 422
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical10045 line 424
  95. def OAI.MUB6.Certificate.PairSemantics.raw10046 line 433
  96. def OAI.MUB6.Certificate.PairSemantics.raw10046step0 line 435
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical10046 line 437
  98. def OAI.MUB6.Certificate.PairSemantics.raw10047 line 446
  99. def OAI.MUB6.Certificate.PairSemantics.raw10047step0 line 448
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical10047 line 450