OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical200.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6400 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical6400 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw6401 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw6401step0 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw6401step1 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw6401step2 line 30
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical6401 line 32
  8. def OAI.MUB6.Certificate.PairSemantics.raw6402 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw6402step0 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw6402step1 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw6402step2 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6402 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw6403 line 74
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6403 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw6404 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6404 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw6405 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw6405step0 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw6405step1 line 90
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6405 line 92
  21. def OAI.MUB6.Certificate.PairSemantics.raw6406 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6406 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw6407 line 111
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6407 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw6408 line 117
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6408 line 119
  27. def OAI.MUB6.Certificate.PairSemantics.raw6409 line 123
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6409 line 125
  29. def OAI.MUB6.Certificate.PairSemantics.raw6410 line 129
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6410 line 131
  31. def OAI.MUB6.Certificate.PairSemantics.raw6411 line 135
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6411 line 137
  33. def OAI.MUB6.Certificate.PairSemantics.raw6412 line 141
  34. def OAI.MUB6.Certificate.PairSemantics.raw6412step0 line 143
  35. def OAI.MUB6.Certificate.PairSemantics.raw6412step1 line 145
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6412 line 147
  37. def OAI.MUB6.Certificate.PairSemantics.raw6413 line 160
  38. def OAI.MUB6.Certificate.PairSemantics.raw6413step0 line 162
  39. def OAI.MUB6.Certificate.PairSemantics.raw6413step1 line 164
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6413 line 166
  41. def OAI.MUB6.Certificate.PairSemantics.raw6414 line 179
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6414 line 181
  43. def OAI.MUB6.Certificate.PairSemantics.raw6415 line 185
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6415 line 187
  45. def OAI.MUB6.Certificate.PairSemantics.raw6416 line 191
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6416 line 193
  47. def OAI.MUB6.Certificate.PairSemantics.raw6417 line 197
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6417 line 199
  49. def OAI.MUB6.Certificate.PairSemantics.raw6418 line 203
  50. def OAI.MUB6.Certificate.PairSemantics.raw6418step0 line 205
  51. def OAI.MUB6.Certificate.PairSemantics.raw6418step1 line 207
  52. def OAI.MUB6.Certificate.PairSemantics.raw6418step2 line 209
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical6418 line 211
  54. def OAI.MUB6.Certificate.PairSemantics.raw6419 line 228
  55. def OAI.MUB6.Certificate.PairSemantics.raw6419step0 line 230
  56. def OAI.MUB6.Certificate.PairSemantics.raw6419step1 line 232
  57. def OAI.MUB6.Certificate.PairSemantics.raw6419step2 line 234
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6419 line 236
  59. def OAI.MUB6.Certificate.PairSemantics.raw6420 line 253
  60. def OAI.MUB6.Certificate.PairSemantics.raw6420step0 line 255
  61. def OAI.MUB6.Certificate.PairSemantics.raw6420step1 line 257
  62. def OAI.MUB6.Certificate.PairSemantics.raw6420step2 line 259
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6420 line 261
  64. def OAI.MUB6.Certificate.PairSemantics.raw6421 line 278
  65. def OAI.MUB6.Certificate.PairSemantics.raw6421step0 line 280
  66. def OAI.MUB6.Certificate.PairSemantics.raw6421step1 line 282
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6421 line 284
  68. def OAI.MUB6.Certificate.PairSemantics.raw6422 line 297
  69. def OAI.MUB6.Certificate.PairSemantics.raw6422step0 line 299
  70. def OAI.MUB6.Certificate.PairSemantics.raw6422step1 line 301
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6422 line 303
  72. def OAI.MUB6.Certificate.PairSemantics.raw6423 line 316
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6423 line 318
  74. def OAI.MUB6.Certificate.PairSemantics.raw6424 line 322
  75. def OAI.MUB6.Certificate.PairSemantics.raw6424step0 line 324
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6424 line 326
  77. def OAI.MUB6.Certificate.PairSemantics.raw6425 line 335
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6425 line 337
  79. def OAI.MUB6.Certificate.PairSemantics.raw6426 line 341
  80. def OAI.MUB6.Certificate.PairSemantics.raw6426step0 line 343
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6426 line 345
  82. def OAI.MUB6.Certificate.PairSemantics.raw6427 line 354
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6427 line 356
  84. def OAI.MUB6.Certificate.PairSemantics.raw6428 line 360
  85. def OAI.MUB6.Certificate.PairSemantics.raw6428step0 line 362
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6428 line 364
  87. def OAI.MUB6.Certificate.PairSemantics.raw6429 line 373
  88. def OAI.MUB6.Certificate.PairSemantics.raw6429step0 line 375
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6429 line 377
  90. def OAI.MUB6.Certificate.PairSemantics.raw6430 line 386
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6430 line 388
  92. def OAI.MUB6.Certificate.PairSemantics.raw6431 line 392
  93. def OAI.MUB6.Certificate.PairSemantics.raw6431step0 line 394
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical6431 line 396