OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical266.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8512 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw8512step0 line 25
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8512 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw8513 line 36
  5. def OAI.MUB6.Certificate.PairSemantics.raw8513step0 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw8513step1 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw8513step2 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8513 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw8514 line 62
  10. def OAI.MUB6.Certificate.PairSemantics.raw8514step0 line 64
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical8514 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw8515 line 75
  13. def OAI.MUB6.Certificate.PairSemantics.raw8515step0 line 77
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8515 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw8516 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw8516step0 line 90
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8516 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw8517 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw8517step0 line 103
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8517 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw8518 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw8518step0 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw8518step1 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8518 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw8519 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw8519step0 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw8519step1 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8519 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw8520 line 153
  30. def OAI.MUB6.Certificate.PairSemantics.raw8520step0 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw8520step1 line 157
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8520 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw8521 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw8521step0 line 174
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8521 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw8522 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw8522step0 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw8522step1 line 189
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8522 line 191
  40. def OAI.MUB6.Certificate.PairSemantics.raw8523 line 204
  41. def OAI.MUB6.Certificate.PairSemantics.raw8523step0 line 206
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8523 line 208
  43. def OAI.MUB6.Certificate.PairSemantics.raw8524 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw8524step0 line 219
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8524 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw8525 line 230
  47. def OAI.MUB6.Certificate.PairSemantics.raw8525step0 line 232
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8525 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw8526 line 243
  50. def OAI.MUB6.Certificate.PairSemantics.raw8526step0 line 245
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8526 line 247
  52. def OAI.MUB6.Certificate.PairSemantics.raw8527 line 256
  53. def OAI.MUB6.Certificate.PairSemantics.raw8527step0 line 258
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8527 line 260
  55. def OAI.MUB6.Certificate.PairSemantics.raw8528 line 269
  56. def OAI.MUB6.Certificate.PairSemantics.raw8528step0 line 271
  57. def OAI.MUB6.Certificate.PairSemantics.raw8528step1 line 273
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8528 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw8529 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw8529step0 line 290
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8529 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw8530 line 301
  63. def OAI.MUB6.Certificate.PairSemantics.raw8530step0 line 303
  64. def OAI.MUB6.Certificate.PairSemantics.raw8530step1 line 305
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8530 line 307
  66. def OAI.MUB6.Certificate.PairSemantics.raw8531 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw8531step0 line 322
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8531 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw8532 line 333
  70. def OAI.MUB6.Certificate.PairSemantics.raw8532step0 line 335
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8532 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw8533 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw8533step0 line 348
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical8533 line 350
  75. def OAI.MUB6.Certificate.PairSemantics.raw8534 line 359
  76. def OAI.MUB6.Certificate.PairSemantics.raw8534step0 line 361
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8534 line 363
  78. def OAI.MUB6.Certificate.PairSemantics.raw8535 line 372
  79. def OAI.MUB6.Certificate.PairSemantics.raw8535step0 line 374
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical8535 line 376
  81. def OAI.MUB6.Certificate.PairSemantics.raw8536 line 385
  82. def OAI.MUB6.Certificate.PairSemantics.raw8536step0 line 387
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8536 line 389
  84. def OAI.MUB6.Certificate.PairSemantics.raw8537 line 398
  85. def OAI.MUB6.Certificate.PairSemantics.raw8537step0 line 400
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8537 line 402
  87. def OAI.MUB6.Certificate.PairSemantics.raw8538 line 411
  88. def OAI.MUB6.Certificate.PairSemantics.raw8538step0 line 413
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8538 line 415
  90. def OAI.MUB6.Certificate.PairSemantics.raw8539 line 424
  91. def OAI.MUB6.Certificate.PairSemantics.raw8539step0 line 426
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical8539 line 428
  93. def OAI.MUB6.Certificate.PairSemantics.raw8540 line 437
  94. def OAI.MUB6.Certificate.PairSemantics.raw8540step0 line 439
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical8540 line 441
  96. def OAI.MUB6.Certificate.PairSemantics.raw8541 line 450
  97. def OAI.MUB6.Certificate.PairSemantics.raw8541step0 line 452
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical8541 line 454
  99. def OAI.MUB6.Certificate.PairSemantics.raw8542 line 463
  100. def OAI.MUB6.Certificate.PairSemantics.raw8542step0 line 465
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8542 line 467
  102. def OAI.MUB6.Certificate.PairSemantics.raw8543 line 476
  103. def OAI.MUB6.Certificate.PairSemantics.raw8543step0 line 478
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8543 line 480