OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical287.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9184 line 27
  2. def OAI.MUB6.Certificate.PairSemantics.raw9184step0 line 29
  3. def OAI.MUB6.Certificate.PairSemantics.raw9184step1 line 31
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9184 line 33
  5. def OAI.MUB6.Certificate.PairSemantics.raw9185 line 46
  6. def OAI.MUB6.Certificate.PairSemantics.raw9185step0 line 48
  7. def OAI.MUB6.Certificate.PairSemantics.raw9185step1 line 50
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9185 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw9186 line 65
  10. def OAI.MUB6.Certificate.PairSemantics.raw9186step0 line 67
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical9186 line 69
  12. def OAI.MUB6.Certificate.PairSemantics.raw9187 line 78
  13. def OAI.MUB6.Certificate.PairSemantics.raw9187step0 line 80
  14. def OAI.MUB6.Certificate.PairSemantics.raw9187step1 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw9187step2 line 84
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical9187 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw9188 line 103
  18. def OAI.MUB6.Certificate.PairSemantics.raw9188step0 line 105
  19. def OAI.MUB6.Certificate.PairSemantics.raw9188step1 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw9188step2 line 109
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9188 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw9189 line 128
  23. def OAI.MUB6.Certificate.PairSemantics.raw9189step0 line 130
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9189 line 132
  25. def OAI.MUB6.Certificate.PairSemantics.raw9190 line 141
  26. def OAI.MUB6.Certificate.PairSemantics.raw9190step0 line 143
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9190 line 145
  28. def OAI.MUB6.Certificate.PairSemantics.raw9191 line 154
  29. def OAI.MUB6.Certificate.PairSemantics.raw9191step0 line 156
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9191 line 158
  31. def OAI.MUB6.Certificate.PairSemantics.raw9192 line 167
  32. def OAI.MUB6.Certificate.PairSemantics.raw9192step0 line 169
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9192 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw9193 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw9193step0 line 182
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9193 line 184
  37. def OAI.MUB6.Certificate.PairSemantics.raw9194 line 193
  38. def OAI.MUB6.Certificate.PairSemantics.raw9194step0 line 195
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9194 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw9195 line 206
  41. def OAI.MUB6.Certificate.PairSemantics.raw9195step0 line 208
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9195 line 210
  43. def OAI.MUB6.Certificate.PairSemantics.raw9196 line 219
  44. def OAI.MUB6.Certificate.PairSemantics.raw9196step0 line 221
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9196 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw9197 line 232
  47. def OAI.MUB6.Certificate.PairSemantics.raw9197step0 line 234
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9197 line 236
  49. def OAI.MUB6.Certificate.PairSemantics.raw9198 line 245
  50. def OAI.MUB6.Certificate.PairSemantics.raw9198step0 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw9198step1 line 249
  52. def OAI.MUB6.Certificate.PairSemantics.raw9198step2 line 251
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9198 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw9199 line 270
  55. def OAI.MUB6.Certificate.PairSemantics.raw9199step0 line 272
  56. def OAI.MUB6.Certificate.PairSemantics.raw9199step1 line 274
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9199 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw9200 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw9200step0 line 291
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical9200 line 293
  61. def OAI.MUB6.Certificate.PairSemantics.raw9201 line 302
  62. def OAI.MUB6.Certificate.PairSemantics.raw9201step0 line 304
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9201 line 306
  64. def OAI.MUB6.Certificate.PairSemantics.raw9202 line 315
  65. def OAI.MUB6.Certificate.PairSemantics.raw9202step0 line 317
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9202 line 319
  67. def OAI.MUB6.Certificate.PairSemantics.raw9203 line 328
  68. def OAI.MUB6.Certificate.PairSemantics.raw9203step0 line 330
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9203 line 332
  70. def OAI.MUB6.Certificate.PairSemantics.raw9204 line 341
  71. def OAI.MUB6.Certificate.PairSemantics.raw9204step0 line 343
  72. def OAI.MUB6.Certificate.PairSemantics.raw9204step1 line 345
  73. def OAI.MUB6.Certificate.PairSemantics.raw9204step2 line 347
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9204 line 349
  75. def OAI.MUB6.Certificate.PairSemantics.raw9205 line 367
  76. def OAI.MUB6.Certificate.PairSemantics.raw9205step0 line 369
  77. def OAI.MUB6.Certificate.PairSemantics.raw9205step1 line 371
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9205 line 373
  79. def OAI.MUB6.Certificate.PairSemantics.raw9206 line 386
  80. def OAI.MUB6.Certificate.PairSemantics.raw9206step0 line 388
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9206 line 390
  82. def OAI.MUB6.Certificate.PairSemantics.raw9207 line 399
  83. def OAI.MUB6.Certificate.PairSemantics.raw9207step0 line 401
  84. def OAI.MUB6.Certificate.PairSemantics.raw9207step1 line 403
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9207 line 405
  86. def OAI.MUB6.Certificate.PairSemantics.raw9208 line 418
  87. def OAI.MUB6.Certificate.PairSemantics.raw9208step0 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw9208step1 line 422
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9208 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw9209 line 437
  91. def OAI.MUB6.Certificate.PairSemantics.raw9209step0 line 439
  92. def OAI.MUB6.Certificate.PairSemantics.raw9209step1 line 441
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9209 line 443
  94. def OAI.MUB6.Certificate.PairSemantics.raw9210 line 456
  95. def OAI.MUB6.Certificate.PairSemantics.raw9210step0 line 458
  96. def OAI.MUB6.Certificate.PairSemantics.raw9210step1 line 460
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9210 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw9211 line 475
  99. def OAI.MUB6.Certificate.PairSemantics.raw9211step0 line 477
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9211 line 479
  101. def OAI.MUB6.Certificate.PairSemantics.raw9212 line 488
  102. def OAI.MUB6.Certificate.PairSemantics.raw9212step0 line 490
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9212 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw9213 line 501
  105. def OAI.MUB6.Certificate.PairSemantics.raw9213step0 line 503
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical9213 line 505
  107. def OAI.MUB6.Certificate.PairSemantics.raw9214 line 514
  108. def OAI.MUB6.Certificate.PairSemantics.raw9214step0 line 516
  109. def OAI.MUB6.Certificate.PairSemantics.raw9214step1 line 518
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical9214 line 520
  111. def OAI.MUB6.Certificate.PairSemantics.raw9215 line 533
  112. def OAI.MUB6.Certificate.PairSemantics.raw9215step0 line 535
  113. def OAI.MUB6.Certificate.PairSemantics.raw9215step1 line 537
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical9215 line 539