OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical36.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1152 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw1152step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw1152step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1152 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw1153 line 33
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1153 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw1154 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw1154step0 line 41
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1154 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw1155 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw1155step0 line 54
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1155 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw1156 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw1156step0 line 67
  15. def OAI.MUB6.Certificate.PairSemantics.raw1156step1 line 69
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1156 line 71
  17. def OAI.MUB6.Certificate.PairSemantics.raw1157 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw1157step0 line 86
  19. def OAI.MUB6.Certificate.PairSemantics.raw1157step1 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw1157step2 line 90
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1157 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw1158 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw1158step0 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw1158step1 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw1158step2 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1158 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw1159 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw1159step0 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw1159step1 line 138
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1159 line 140
  31. def OAI.MUB6.Certificate.PairSemantics.raw1160 line 153
  32. def OAI.MUB6.Certificate.PairSemantics.raw1160step0 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw1160step1 line 157
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1160 line 159
  35. def OAI.MUB6.Certificate.PairSemantics.raw1161 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw1161step0 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw1161step1 line 176
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1161 line 178
  39. def OAI.MUB6.Certificate.PairSemantics.raw1162 line 191
  40. def OAI.MUB6.Certificate.PairSemantics.raw1162step0 line 193
  41. def OAI.MUB6.Certificate.PairSemantics.raw1162step1 line 195
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1162 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw1163 line 210
  44. def OAI.MUB6.Certificate.PairSemantics.raw1163step0 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw1163step1 line 214
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1163 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw1164 line 229
  48. def OAI.MUB6.Certificate.PairSemantics.raw1164step0 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw1164step1 line 233
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1164 line 235
  51. def OAI.MUB6.Certificate.PairSemantics.raw1165 line 248
  52. def OAI.MUB6.Certificate.PairSemantics.raw1165step0 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw1165step1 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw1165step2 line 254
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1165 line 256
  56. def OAI.MUB6.Certificate.PairSemantics.raw1166 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw1166step0 line 275
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1166 line 277
  59. def OAI.MUB6.Certificate.PairSemantics.raw1167 line 286
  60. def OAI.MUB6.Certificate.PairSemantics.raw1167step0 line 288
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1167 line 290
  62. def OAI.MUB6.Certificate.PairSemantics.raw1168 line 299
  63. def OAI.MUB6.Certificate.PairSemantics.raw1168step0 line 301
  64. def OAI.MUB6.Certificate.PairSemantics.raw1168step1 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw1168step2 line 305
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1168 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw1169 line 324
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1169 line 326
  69. def OAI.MUB6.Certificate.PairSemantics.raw1170 line 330
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1170 line 332
  71. def OAI.MUB6.Certificate.PairSemantics.raw1171 line 336
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1171 line 338
  73. def OAI.MUB6.Certificate.PairSemantics.raw1172 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw1172step0 line 344
  75. def OAI.MUB6.Certificate.PairSemantics.raw1172step1 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw1172step2 line 348
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1172 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw1173 line 367
  79. def OAI.MUB6.Certificate.PairSemantics.raw1173step0 line 369
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1173 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw1174 line 380
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1174 line 382
  83. def OAI.MUB6.Certificate.PairSemantics.raw1175 line 386
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical1175 line 388
  85. def OAI.MUB6.Certificate.PairSemantics.raw1176 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw1176step0 line 394
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1176 line 396
  88. def OAI.MUB6.Certificate.PairSemantics.raw1177 line 405
  89. def OAI.MUB6.Certificate.PairSemantics.raw1177step0 line 407
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1177 line 409
  91. def OAI.MUB6.Certificate.PairSemantics.raw1178 line 418
  92. def OAI.MUB6.Certificate.PairSemantics.raw1178step0 line 420
  93. def OAI.MUB6.Certificate.PairSemantics.raw1178step1 line 422
  94. def OAI.MUB6.Certificate.PairSemantics.raw1178step2 line 424
  95. def OAI.MUB6.Certificate.PairSemantics.raw1178step3 line 426
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1178 line 428
  97. def OAI.MUB6.Certificate.PairSemantics.raw1179 line 450
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1179 line 452
  99. def OAI.MUB6.Certificate.PairSemantics.raw1180 line 456
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical1180 line 458
  101. def OAI.MUB6.Certificate.PairSemantics.raw1181 line 462
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical1181 line 464
  103. def OAI.MUB6.Certificate.PairSemantics.raw1182 line 468
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical1182 line 470
  105. def OAI.MUB6.Certificate.PairSemantics.raw1183 line 474
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical1183 line 476