OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical192.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6144 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical6144 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw6145 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw6145step0 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6145 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw6146 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw6146step0 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6146 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw6147 line 48
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6147 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw6148 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw6148step0 line 56
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6148 line 58
  14. def OAI.MUB6.Certificate.PairSemantics.raw6149 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6149 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw6150 line 73
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6150 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw6151 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw6151step0 line 81
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6151 line 83
  21. def OAI.MUB6.Certificate.PairSemantics.raw6152 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw6152step0 line 94
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical6152 line 96
  24. def OAI.MUB6.Certificate.PairSemantics.raw6153 line 105
  25. def OAI.MUB6.Certificate.PairSemantics.raw6153step0 line 107
  26. def OAI.MUB6.Certificate.PairSemantics.raw6153step1 line 109
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6153 line 111
  28. def OAI.MUB6.Certificate.PairSemantics.raw6154 line 124
  29. def OAI.MUB6.Certificate.PairSemantics.raw6154step0 line 126
  30. def OAI.MUB6.Certificate.PairSemantics.raw6154step1 line 128
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6154 line 130
  32. def OAI.MUB6.Certificate.PairSemantics.raw6155 line 143
  33. def OAI.MUB6.Certificate.PairSemantics.raw6155step0 line 145
  34. def OAI.MUB6.Certificate.PairSemantics.raw6155step1 line 147
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6155 line 149
  36. def OAI.MUB6.Certificate.PairSemantics.raw6156 line 162
  37. def OAI.MUB6.Certificate.PairSemantics.raw6156step0 line 164
  38. def OAI.MUB6.Certificate.PairSemantics.raw6156step1 line 166
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6156 line 168
  40. def OAI.MUB6.Certificate.PairSemantics.raw6157 line 181
  41. def OAI.MUB6.Certificate.PairSemantics.raw6157step0 line 183
  42. def OAI.MUB6.Certificate.PairSemantics.raw6157step1 line 185
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6157 line 187
  44. def OAI.MUB6.Certificate.PairSemantics.raw6158 line 200
  45. def OAI.MUB6.Certificate.PairSemantics.raw6158step0 line 202
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6158 line 204
  47. def OAI.MUB6.Certificate.PairSemantics.raw6159 line 213
  48. def OAI.MUB6.Certificate.PairSemantics.raw6159step0 line 215
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6159 line 217
  50. def OAI.MUB6.Certificate.PairSemantics.raw6160 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw6160step0 line 228
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6160 line 230
  53. def OAI.MUB6.Certificate.PairSemantics.raw6161 line 239
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6161 line 241
  55. def OAI.MUB6.Certificate.PairSemantics.raw6162 line 245
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6162 line 247
  57. def OAI.MUB6.Certificate.PairSemantics.raw6163 line 251
  58. def OAI.MUB6.Certificate.PairSemantics.raw6163step0 line 253
  59. def OAI.MUB6.Certificate.PairSemantics.raw6163step1 line 255
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6163 line 257
  61. def OAI.MUB6.Certificate.PairSemantics.raw6164 line 270
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6164 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw6165 line 276
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6165 line 278
  65. def OAI.MUB6.Certificate.PairSemantics.raw6166 line 282
  66. def OAI.MUB6.Certificate.PairSemantics.raw6166step0 line 284
  67. def OAI.MUB6.Certificate.PairSemantics.raw6166step1 line 286
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6166 line 288
  69. def OAI.MUB6.Certificate.PairSemantics.raw6167 line 301
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6167 line 303
  71. def OAI.MUB6.Certificate.PairSemantics.raw6168 line 307
  72. def OAI.MUB6.Certificate.PairSemantics.raw6168step0 line 309
  73. def OAI.MUB6.Certificate.PairSemantics.raw6168step1 line 311
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6168 line 313
  75. def OAI.MUB6.Certificate.PairSemantics.raw6169 line 326
  76. def OAI.MUB6.Certificate.PairSemantics.raw6169step0 line 328
  77. def OAI.MUB6.Certificate.PairSemantics.raw6169step1 line 330
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6169 line 332
  79. def OAI.MUB6.Certificate.PairSemantics.raw6170 line 345
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6170 line 347
  81. def OAI.MUB6.Certificate.PairSemantics.raw6171 line 351
  82. def OAI.MUB6.Certificate.PairSemantics.raw6171step0 line 353
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6171 line 355
  84. def OAI.MUB6.Certificate.PairSemantics.raw6172 line 364
  85. def OAI.MUB6.Certificate.PairSemantics.raw6172step0 line 366
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6172 line 368
  87. def OAI.MUB6.Certificate.PairSemantics.raw6173 line 377
  88. def OAI.MUB6.Certificate.PairSemantics.raw6173step0 line 379
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6173 line 381
  90. def OAI.MUB6.Certificate.PairSemantics.raw6174 line 390
  91. def OAI.MUB6.Certificate.PairSemantics.raw6174step0 line 392
  92. def OAI.MUB6.Certificate.PairSemantics.raw6174step1 line 394
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6174 line 396
  94. def OAI.MUB6.Certificate.PairSemantics.raw6175 line 409
  95. def OAI.MUB6.Certificate.PairSemantics.raw6175step0 line 411
  96. def OAI.MUB6.Certificate.PairSemantics.raw6175step1 line 413
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6175 line 415