OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical267.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8544 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw8544step0 line 24
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8544 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw8545 line 35
  5. def OAI.MUB6.Certificate.PairSemantics.raw8545step0 line 37
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8545 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw8546 line 48
  8. def OAI.MUB6.Certificate.PairSemantics.raw8546step0 line 50
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8546 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw8547 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw8547step0 line 63
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8547 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw8548 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw8548step0 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw8548step1 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8548 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw8549 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw8549step0 line 96
  19. def OAI.MUB6.Certificate.PairSemantics.raw8549step1 line 98
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8549 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw8550 line 113
  22. def OAI.MUB6.Certificate.PairSemantics.raw8550step0 line 115
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8550 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw8551 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw8551step0 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw8551step1 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8551 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw8552 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw8552step0 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw8552step1 line 149
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8552 line 151
  32. def OAI.MUB6.Certificate.PairSemantics.raw8553 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw8553step0 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw8553step1 line 168
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8553 line 170
  36. def OAI.MUB6.Certificate.PairSemantics.raw8554 line 183
  37. def OAI.MUB6.Certificate.PairSemantics.raw8554step0 line 185
  38. def OAI.MUB6.Certificate.PairSemantics.raw8554step1 line 187
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8554 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw8555 line 203
  41. def OAI.MUB6.Certificate.PairSemantics.raw8555step0 line 205
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8555 line 207
  43. def OAI.MUB6.Certificate.PairSemantics.raw8556 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw8556step0 line 218
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8556 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw8557 line 229
  47. def OAI.MUB6.Certificate.PairSemantics.raw8557step0 line 231
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8557 line 233
  49. def OAI.MUB6.Certificate.PairSemantics.raw8558 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw8558step0 line 244
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8558 line 246
  52. def OAI.MUB6.Certificate.PairSemantics.raw8559 line 255
  53. def OAI.MUB6.Certificate.PairSemantics.raw8559step0 line 257
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8559 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw8560 line 268
  56. def OAI.MUB6.Certificate.PairSemantics.raw8560step0 line 270
  57. def OAI.MUB6.Certificate.PairSemantics.raw8560step1 line 272
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8560 line 274
  59. def OAI.MUB6.Certificate.PairSemantics.raw8561 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw8561step0 line 290
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8561 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw8562 line 301
  63. def OAI.MUB6.Certificate.PairSemantics.raw8562step0 line 303
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8562 line 305
  65. def OAI.MUB6.Certificate.PairSemantics.raw8563 line 314
  66. def OAI.MUB6.Certificate.PairSemantics.raw8563step0 line 316
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical8563 line 318
  68. def OAI.MUB6.Certificate.PairSemantics.raw8564 line 327
  69. def OAI.MUB6.Certificate.PairSemantics.raw8564step0 line 329
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8564 line 331
  71. def OAI.MUB6.Certificate.PairSemantics.raw8565 line 340
  72. def OAI.MUB6.Certificate.PairSemantics.raw8565step0 line 342
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8565 line 344
  74. def OAI.MUB6.Certificate.PairSemantics.raw8566 line 353
  75. def OAI.MUB6.Certificate.PairSemantics.raw8566step0 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw8566step1 line 357
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8566 line 359
  78. def OAI.MUB6.Certificate.PairSemantics.raw8567 line 372
  79. def OAI.MUB6.Certificate.PairSemantics.raw8567step0 line 374
  80. def OAI.MUB6.Certificate.PairSemantics.raw8567step1 line 376
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8567 line 378
  82. def OAI.MUB6.Certificate.PairSemantics.raw8568 line 391
  83. def OAI.MUB6.Certificate.PairSemantics.raw8568step0 line 393
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8568 line 395
  85. def OAI.MUB6.Certificate.PairSemantics.raw8569 line 404
  86. def OAI.MUB6.Certificate.PairSemantics.raw8569step0 line 406
  87. def OAI.MUB6.Certificate.PairSemantics.raw8569step1 line 408
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8569 line 410
  89. def OAI.MUB6.Certificate.PairSemantics.raw8570 line 423
  90. def OAI.MUB6.Certificate.PairSemantics.raw8570step0 line 425
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8570 line 427
  92. def OAI.MUB6.Certificate.PairSemantics.raw8571 line 436
  93. def OAI.MUB6.Certificate.PairSemantics.raw8571step0 line 438
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8571 line 440
  95. def OAI.MUB6.Certificate.PairSemantics.raw8572 line 449
  96. def OAI.MUB6.Certificate.PairSemantics.raw8572step0 line 451
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical8572 line 453
  98. def OAI.MUB6.Certificate.PairSemantics.raw8573 line 462
  99. def OAI.MUB6.Certificate.PairSemantics.raw8573step0 line 464
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical8573 line 466
  101. def OAI.MUB6.Certificate.PairSemantics.raw8574 line 475
  102. def OAI.MUB6.Certificate.PairSemantics.raw8574step0 line 477
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical8574 line 479
  104. def OAI.MUB6.Certificate.PairSemantics.raw8575 line 488
  105. def OAI.MUB6.Certificate.PairSemantics.raw8575step0 line 490
  106. def OAI.MUB6.Certificate.PairSemantics.raw8575step1 line 492
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8575 line 494