OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical219.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7008 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw7008step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical7008 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw7009 line 32
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical7009 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw7010 line 38
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical7010 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw7011 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw7011step0 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7011 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw7012 line 57
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7012 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw7013 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw7013step0 line 65
  15. def OAI.MUB6.Certificate.PairSemantics.raw7013step1 line 67
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7013 line 69
  17. def OAI.MUB6.Certificate.PairSemantics.raw7014 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw7014step0 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw7014step1 line 86
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7014 line 88
  21. def OAI.MUB6.Certificate.PairSemantics.raw7015 line 101
  22. def OAI.MUB6.Certificate.PairSemantics.raw7015step0 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw7015step1 line 105
  24. def OAI.MUB6.Certificate.PairSemantics.raw7015step2 line 107
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7015 line 109
  26. def OAI.MUB6.Certificate.PairSemantics.raw7016 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw7016step0 line 128
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7016 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw7017 line 140
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7017 line 142
  31. def OAI.MUB6.Certificate.PairSemantics.raw7018 line 146
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7018 line 148
  33. def OAI.MUB6.Certificate.PairSemantics.raw7019 line 152
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7019 line 154
  35. def OAI.MUB6.Certificate.PairSemantics.raw7020 line 158
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7020 line 160
  37. def OAI.MUB6.Certificate.PairSemantics.raw7021 line 164
  38. def OAI.MUB6.Certificate.PairSemantics.raw7021step0 line 166
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7021 line 168
  40. def OAI.MUB6.Certificate.PairSemantics.raw7022 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw7022step0 line 180
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7022 line 182
  43. def OAI.MUB6.Certificate.PairSemantics.raw7023 line 192
  44. def OAI.MUB6.Certificate.PairSemantics.raw7023step0 line 194
  45. def OAI.MUB6.Certificate.PairSemantics.raw7023step1 line 196
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical7023 line 198
  47. def OAI.MUB6.Certificate.PairSemantics.raw7024 line 211
  48. def OAI.MUB6.Certificate.PairSemantics.raw7024step0 line 213
  49. def OAI.MUB6.Certificate.PairSemantics.raw7024step1 line 215
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7024 line 217
  51. def OAI.MUB6.Certificate.PairSemantics.raw7025 line 230
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7025 line 232
  53. def OAI.MUB6.Certificate.PairSemantics.raw7026 line 236
  54. def OAI.MUB6.Certificate.PairSemantics.raw7026step0 line 238
  55. def OAI.MUB6.Certificate.PairSemantics.raw7026step1 line 240
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical7026 line 242
  57. def OAI.MUB6.Certificate.PairSemantics.raw7027 line 255
  58. def OAI.MUB6.Certificate.PairSemantics.raw7027step0 line 257
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7027 line 259
  60. def OAI.MUB6.Certificate.PairSemantics.raw7028 line 268
  61. def OAI.MUB6.Certificate.PairSemantics.raw7028step0 line 270
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7028 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw7029 line 281
  64. def OAI.MUB6.Certificate.PairSemantics.raw7029step0 line 283
  65. def OAI.MUB6.Certificate.PairSemantics.raw7029step1 line 285
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7029 line 287
  67. def OAI.MUB6.Certificate.PairSemantics.raw7030 line 300
  68. def OAI.MUB6.Certificate.PairSemantics.raw7030step0 line 302
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7030 line 304
  70. def OAI.MUB6.Certificate.PairSemantics.raw7031 line 313
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7031 line 315
  72. def OAI.MUB6.Certificate.PairSemantics.raw7032 line 319
  73. def OAI.MUB6.Certificate.PairSemantics.raw7032step0 line 321
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7032 line 323
  75. def OAI.MUB6.Certificate.PairSemantics.raw7033 line 332
  76. def OAI.MUB6.Certificate.PairSemantics.raw7033step0 line 334
  77. def OAI.MUB6.Certificate.PairSemantics.raw7033step1 line 336
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7033 line 338
  79. def OAI.MUB6.Certificate.PairSemantics.raw7034 line 351
  80. def OAI.MUB6.Certificate.PairSemantics.raw7034step0 line 353
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical7034 line 355
  82. def OAI.MUB6.Certificate.PairSemantics.raw7035 line 364
  83. def OAI.MUB6.Certificate.PairSemantics.raw7035step0 line 366
  84. def OAI.MUB6.Certificate.PairSemantics.raw7035step1 line 368
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7035 line 370
  86. def OAI.MUB6.Certificate.PairSemantics.raw7036 line 383
  87. def OAI.MUB6.Certificate.PairSemantics.raw7036step0 line 385
  88. def OAI.MUB6.Certificate.PairSemantics.raw7036step1 line 387
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7036 line 389
  90. def OAI.MUB6.Certificate.PairSemantics.raw7037 line 402
  91. def OAI.MUB6.Certificate.PairSemantics.raw7037step0 line 404
  92. def OAI.MUB6.Certificate.PairSemantics.raw7037step1 line 406
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7037 line 408
  94. def OAI.MUB6.Certificate.PairSemantics.raw7038 line 421
  95. def OAI.MUB6.Certificate.PairSemantics.raw7038step0 line 423
  96. def OAI.MUB6.Certificate.PairSemantics.raw7038step1 line 425
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7038 line 427
  98. def OAI.MUB6.Certificate.PairSemantics.raw7039 line 440
  99. def OAI.MUB6.Certificate.PairSemantics.raw7039step0 line 442
  100. def OAI.MUB6.Certificate.PairSemantics.raw7039step1 line 444
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7039 line 446