OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical37.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1184 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1184 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1185 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw1185step0 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1185 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw1186 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1186 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw1187 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw1187step0 line 43
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1187 line 45
  11. def OAI.MUB6.Certificate.PairSemantics.raw1188 line 54
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1188 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw1189 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw1189step0 line 62
  15. def OAI.MUB6.Certificate.PairSemantics.raw1189step1 line 64
  16. def OAI.MUB6.Certificate.PairSemantics.raw1189step2 line 66
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1189 line 68
  18. def OAI.MUB6.Certificate.PairSemantics.raw1190 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw1190step0 line 87
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1190 line 89
  21. def OAI.MUB6.Certificate.PairSemantics.raw1191 line 98
  22. def OAI.MUB6.Certificate.PairSemantics.raw1191step0 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw1191step1 line 102
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1191 line 104
  25. def OAI.MUB6.Certificate.PairSemantics.raw1192 line 117
  26. def OAI.MUB6.Certificate.PairSemantics.raw1192step0 line 119
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1192 line 121
  28. def OAI.MUB6.Certificate.PairSemantics.raw1193 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw1193step0 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw1193step1 line 134
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1193 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw1194 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw1194step0 line 151
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1194 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw1195 line 162
  36. def OAI.MUB6.Certificate.PairSemantics.raw1195step0 line 164
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1195 line 166
  38. def OAI.MUB6.Certificate.PairSemantics.raw1196 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw1196step0 line 177
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1196 line 179
  41. def OAI.MUB6.Certificate.PairSemantics.raw1197 line 188
  42. def OAI.MUB6.Certificate.PairSemantics.raw1197step0 line 190
  43. def OAI.MUB6.Certificate.PairSemantics.raw1197step1 line 192
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1197 line 194
  45. def OAI.MUB6.Certificate.PairSemantics.raw1198 line 207
  46. def OAI.MUB6.Certificate.PairSemantics.raw1198step0 line 209
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1198 line 211
  48. def OAI.MUB6.Certificate.PairSemantics.raw1199 line 220
  49. def OAI.MUB6.Certificate.PairSemantics.raw1199step0 line 222
  50. def OAI.MUB6.Certificate.PairSemantics.raw1199step1 line 224
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1199 line 226
  52. def OAI.MUB6.Certificate.PairSemantics.raw1200 line 239
  53. def OAI.MUB6.Certificate.PairSemantics.raw1200step0 line 241
  54. def OAI.MUB6.Certificate.PairSemantics.raw1200step1 line 243
  55. def OAI.MUB6.Certificate.PairSemantics.raw1200step2 line 245
  56. def OAI.MUB6.Certificate.PairSemantics.raw1200step3 line 247
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1200 line 249
  58. def OAI.MUB6.Certificate.PairSemantics.raw1201 line 271
  59. def OAI.MUB6.Certificate.PairSemantics.raw1201step0 line 273
  60. def OAI.MUB6.Certificate.PairSemantics.raw1201step1 line 275
  61. def OAI.MUB6.Certificate.PairSemantics.raw1201step2 line 277
  62. def OAI.MUB6.Certificate.PairSemantics.raw1201step3 line 279
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1201 line 281
  64. def OAI.MUB6.Certificate.PairSemantics.raw1202 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw1202step0 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw1202step1 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw1202step2 line 309
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1202 line 311
  69. def OAI.MUB6.Certificate.PairSemantics.raw1203 line 329
  70. def OAI.MUB6.Certificate.PairSemantics.raw1203step0 line 331
  71. def OAI.MUB6.Certificate.PairSemantics.raw1203step1 line 333
  72. def OAI.MUB6.Certificate.PairSemantics.raw1203step2 line 335
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1203 line 337
  74. def OAI.MUB6.Certificate.PairSemantics.raw1204 line 355
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1204 line 357
  76. def OAI.MUB6.Certificate.PairSemantics.raw1205 line 361
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1205 line 363
  78. def OAI.MUB6.Certificate.PairSemantics.raw1206 line 367
  79. def OAI.MUB6.Certificate.PairSemantics.raw1206step0 line 369
  80. def OAI.MUB6.Certificate.PairSemantics.raw1206step1 line 371
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical1206 line 373
  82. def OAI.MUB6.Certificate.PairSemantics.raw1207 line 386
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1207 line 388
  84. def OAI.MUB6.Certificate.PairSemantics.raw1208 line 392
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1208 line 394
  86. def OAI.MUB6.Certificate.PairSemantics.raw1209 line 398
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1209 line 400
  88. def OAI.MUB6.Certificate.PairSemantics.raw1210 line 404
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1210 line 406
  90. def OAI.MUB6.Certificate.PairSemantics.raw1211 line 410
  91. def OAI.MUB6.Certificate.PairSemantics.raw1211step0 line 412
  92. def OAI.MUB6.Certificate.PairSemantics.raw1211step1 line 414
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1211 line 416
  94. def OAI.MUB6.Certificate.PairSemantics.raw1212 line 429
  95. def OAI.MUB6.Certificate.PairSemantics.raw1212step0 line 431
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1212 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw1213 line 442
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1213 line 444
  99. def OAI.MUB6.Certificate.PairSemantics.raw1214 line 448
  100. def OAI.MUB6.Certificate.PairSemantics.raw1214step0 line 450
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical1214 line 452
  102. def OAI.MUB6.Certificate.PairSemantics.raw1215 line 461
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical1215 line 463