OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical1.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw32 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw32step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw32step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical32 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw33 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw33step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw33step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical33 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw34 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw34step0 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical34 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw35 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw35step0 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw35step1 line 71
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical35 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw36 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw36step0 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical36 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw37 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw37step0 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical37 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw38 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw38step0 line 116
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical38 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw39 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw39step0 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical39 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw40 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw40step0 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical40 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw41 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw41step0 line 158
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical41 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw42 line 170
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical42 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw43 line 176
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical43 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw44 line 182
  39. def OAI.MUB6.Certificate.PairSemantics.raw44step0 line 184
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical44 line 186
  41. def OAI.MUB6.Certificate.PairSemantics.raw45 line 195
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical45 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw46 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw46step0 line 203
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical46 line 205
  46. def OAI.MUB6.Certificate.PairSemantics.raw47 line 214
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical47 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw48 line 220
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical48 line 222
  50. def OAI.MUB6.Certificate.PairSemantics.raw49 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw49step0 line 228
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical49 line 230
  53. def OAI.MUB6.Certificate.PairSemantics.raw50 line 239
  54. def OAI.MUB6.Certificate.PairSemantics.raw50step0 line 241
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical50 line 243
  56. def OAI.MUB6.Certificate.PairSemantics.raw51 line 252
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical51 line 254
  58. def OAI.MUB6.Certificate.PairSemantics.raw52 line 258
  59. def OAI.MUB6.Certificate.PairSemantics.raw52step0 line 260
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical52 line 262
  61. def OAI.MUB6.Certificate.PairSemantics.raw53 line 271
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical53 line 273
  63. def OAI.MUB6.Certificate.PairSemantics.raw54 line 277
  64. def OAI.MUB6.Certificate.PairSemantics.raw54step0 line 279
  65. def OAI.MUB6.Certificate.PairSemantics.raw54step1 line 281
  66. def OAI.MUB6.Certificate.PairSemantics.raw54step2 line 283
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical54 line 285
  68. def OAI.MUB6.Certificate.PairSemantics.raw55 line 302
  69. def OAI.MUB6.Certificate.PairSemantics.raw55step0 line 304
  70. def OAI.MUB6.Certificate.PairSemantics.raw55step1 line 306
  71. def OAI.MUB6.Certificate.PairSemantics.raw55step2 line 308
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical55 line 310
  73. def OAI.MUB6.Certificate.PairSemantics.raw56 line 327
  74. def OAI.MUB6.Certificate.PairSemantics.raw56step0 line 329
  75. def OAI.MUB6.Certificate.PairSemantics.raw56step1 line 331
  76. def OAI.MUB6.Certificate.PairSemantics.raw56step2 line 333
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical56 line 335
  78. def OAI.MUB6.Certificate.PairSemantics.raw57 line 352
  79. def OAI.MUB6.Certificate.PairSemantics.raw57step0 line 354
  80. def OAI.MUB6.Certificate.PairSemantics.raw57step1 line 356
  81. def OAI.MUB6.Certificate.PairSemantics.raw57step2 line 358
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical57 line 360
  83. def OAI.MUB6.Certificate.PairSemantics.raw58 line 377
  84. def OAI.MUB6.Certificate.PairSemantics.raw58step0 line 379
  85. def OAI.MUB6.Certificate.PairSemantics.raw58step1 line 381
  86. def OAI.MUB6.Certificate.PairSemantics.raw58step2 line 383
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical58 line 385
  88. def OAI.MUB6.Certificate.PairSemantics.raw59 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw59step0 line 404
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical59 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw60 line 415
  92. def OAI.MUB6.Certificate.PairSemantics.raw60step0 line 417
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical60 line 419
  94. def OAI.MUB6.Certificate.PairSemantics.raw61 line 428
  95. def OAI.MUB6.Certificate.PairSemantics.raw61step0 line 430
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical61 line 432
  97. def OAI.MUB6.Certificate.PairSemantics.raw62 line 441
  98. def OAI.MUB6.Certificate.PairSemantics.raw62step0 line 443
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical62 line 445
  100. def OAI.MUB6.Certificate.PairSemantics.raw63 line 454
  101. def OAI.MUB6.Certificate.PairSemantics.raw63step0 line 456
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical63 line 458