OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical14.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw448 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw448step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw448step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical448 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw449 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw449step0 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw449step1 line 40
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical449 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw450 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw450step0 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw450step1 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical450 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw451 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw451step0 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw451step1 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical451 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw452 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw452step0 line 95
  19. def OAI.MUB6.Certificate.PairSemantics.raw452step1 line 97
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical452 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw453 line 112
  22. def OAI.MUB6.Certificate.PairSemantics.raw453step0 line 114
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical453 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw454 line 125
  25. def OAI.MUB6.Certificate.PairSemantics.raw454step0 line 127
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical454 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw455 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw455step0 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical455 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw456 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw456step0 line 153
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical456 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw457 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw457step0 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw457step1 line 168
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical457 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw458 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw458step0 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw458step1 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical458 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw459 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw459step0 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw459step1 line 206
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical459 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw460 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw460step0 line 223
  47. def OAI.MUB6.Certificate.PairSemantics.raw460step1 line 225
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical460 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw461 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw461step0 line 242
  51. def OAI.MUB6.Certificate.PairSemantics.raw461step1 line 244
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical461 line 246
  53. def OAI.MUB6.Certificate.PairSemantics.raw462 line 259
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical462 line 261
  55. def OAI.MUB6.Certificate.PairSemantics.raw463 line 265
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical463 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw464 line 271
  58. def OAI.MUB6.Certificate.PairSemantics.raw464step0 line 273
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical464 line 275
  60. def OAI.MUB6.Certificate.PairSemantics.raw465 line 284
  61. def OAI.MUB6.Certificate.PairSemantics.raw465step0 line 286
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical465 line 288
  63. def OAI.MUB6.Certificate.PairSemantics.raw466 line 297
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical466 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw467 line 303
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical467 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw468 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw468step0 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical468 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw469 line 322
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical469 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw470 line 328
  73. def OAI.MUB6.Certificate.PairSemantics.raw470step0 line 330
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical470 line 332
  75. def OAI.MUB6.Certificate.PairSemantics.raw471 line 341
  76. def OAI.MUB6.Certificate.PairSemantics.raw471step0 line 343
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical471 line 345
  78. def OAI.MUB6.Certificate.PairSemantics.raw472 line 354
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical472 line 356
  80. def OAI.MUB6.Certificate.PairSemantics.raw473 line 360
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical473 line 362
  82. def OAI.MUB6.Certificate.PairSemantics.raw474 line 366
  83. def OAI.MUB6.Certificate.PairSemantics.raw474step0 line 368
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical474 line 370
  85. def OAI.MUB6.Certificate.PairSemantics.raw475 line 379
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical475 line 381
  87. def OAI.MUB6.Certificate.PairSemantics.raw476 line 385
  88. def OAI.MUB6.Certificate.PairSemantics.raw476step0 line 387
  89. def OAI.MUB6.Certificate.PairSemantics.raw476step1 line 389
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical476 line 391
  91. def OAI.MUB6.Certificate.PairSemantics.raw477 line 404
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical477 line 406
  93. def OAI.MUB6.Certificate.PairSemantics.raw478 line 410
  94. def OAI.MUB6.Certificate.PairSemantics.raw478step0 line 412
  95. def OAI.MUB6.Certificate.PairSemantics.raw478step1 line 414
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical478 line 416
  97. def OAI.MUB6.Certificate.PairSemantics.raw479 line 429
  98. def OAI.MUB6.Certificate.PairSemantics.raw479step0 line 431
  99. def OAI.MUB6.Certificate.PairSemantics.raw479step1 line 433
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical479 line 435