OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical264.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8448 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw8448step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw8448step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8448 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw8449 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw8449step0 line 41
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical8449 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw8450 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw8450step0 line 54
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8450 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw8451 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw8451step0 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8451 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw8452 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw8452step0 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8452 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw8453 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw8453step0 line 93
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8453 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw8454 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw8454step0 line 106
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical8454 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw8455 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw8455step0 line 119
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8455 line 121
  26. def OAI.MUB6.Certificate.PairSemantics.raw8456 line 130
  27. def OAI.MUB6.Certificate.PairSemantics.raw8456step0 line 132
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8456 line 134
  29. def OAI.MUB6.Certificate.PairSemantics.raw8457 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw8457step0 line 145
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8457 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw8458 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw8458step0 line 158
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8458 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw8459 line 169
  36. def OAI.MUB6.Certificate.PairSemantics.raw8459step0 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw8459step1 line 173
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8459 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw8460 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw8460step0 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw8460step1 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw8460step2 line 195
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical8460 line 197
  44. def OAI.MUB6.Certificate.PairSemantics.raw8461 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw8461step0 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw8461step1 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw8461step2 line 221
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8461 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw8462 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw8462step0 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw8462step1 line 245
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical8462 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw8463 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw8463step0 line 262
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8463 line 264
  56. def OAI.MUB6.Certificate.PairSemantics.raw8464 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw8464step0 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw8464step1 line 277
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8464 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw8465 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw8465step0 line 294
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8465 line 296
  63. def OAI.MUB6.Certificate.PairSemantics.raw8466 line 305
  64. def OAI.MUB6.Certificate.PairSemantics.raw8466step0 line 307
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8466 line 309
  66. def OAI.MUB6.Certificate.PairSemantics.raw8467 line 318
  67. def OAI.MUB6.Certificate.PairSemantics.raw8467step0 line 320
  68. def OAI.MUB6.Certificate.PairSemantics.raw8467step1 line 322
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8467 line 324
  70. def OAI.MUB6.Certificate.PairSemantics.raw8468 line 337
  71. def OAI.MUB6.Certificate.PairSemantics.raw8468step0 line 339
  72. def OAI.MUB6.Certificate.PairSemantics.raw8468step1 line 341
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8468 line 343
  74. def OAI.MUB6.Certificate.PairSemantics.raw8469 line 356
  75. def OAI.MUB6.Certificate.PairSemantics.raw8469step0 line 358
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8469 line 360
  77. def OAI.MUB6.Certificate.PairSemantics.raw8470 line 369
  78. def OAI.MUB6.Certificate.PairSemantics.raw8470step0 line 371
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8470 line 373
  80. def OAI.MUB6.Certificate.PairSemantics.raw8471 line 382
  81. def OAI.MUB6.Certificate.PairSemantics.raw8471step0 line 384
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8471 line 386
  83. def OAI.MUB6.Certificate.PairSemantics.raw8472 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw8472step0 line 397
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8472 line 399
  86. def OAI.MUB6.Certificate.PairSemantics.raw8473 line 408
  87. def OAI.MUB6.Certificate.PairSemantics.raw8473step0 line 410
  88. def OAI.MUB6.Certificate.PairSemantics.raw8473step1 line 412
  89. def OAI.MUB6.Certificate.PairSemantics.raw8473step2 line 414
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical8473 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw8474 line 433
  92. def OAI.MUB6.Certificate.PairSemantics.raw8474step0 line 435
  93. def OAI.MUB6.Certificate.PairSemantics.raw8474step1 line 437
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8474 line 439
  95. def OAI.MUB6.Certificate.PairSemantics.raw8475 line 452
  96. def OAI.MUB6.Certificate.PairSemantics.raw8475step0 line 454
  97. def OAI.MUB6.Certificate.PairSemantics.raw8475step1 line 456
  98. def OAI.MUB6.Certificate.PairSemantics.raw8475step2 line 458
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8475 line 460
  100. def OAI.MUB6.Certificate.PairSemantics.raw8476 line 477
  101. def OAI.MUB6.Certificate.PairSemantics.raw8476step0 line 479
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8476 line 481
  103. def OAI.MUB6.Certificate.PairSemantics.raw8477 line 490
  104. def OAI.MUB6.Certificate.PairSemantics.raw8477step0 line 492
  105. def OAI.MUB6.Certificate.PairSemantics.raw8477step1 line 494
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8477 line 496
  107. def OAI.MUB6.Certificate.PairSemantics.raw8478 line 510
  108. def OAI.MUB6.Certificate.PairSemantics.raw8478step0 line 512
  109. def OAI.MUB6.Certificate.PairSemantics.raw8478step1 line 514
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8478 line 516
  111. def OAI.MUB6.Certificate.PairSemantics.raw8479 line 531
  112. def OAI.MUB6.Certificate.PairSemantics.raw8479step0 line 533
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical8479 line 535