OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical207.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6624 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw6624step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw6624step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6624 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw6625 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw6625step0 line 37
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical6625 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw6626 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw6626step0 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw6626step1 line 52
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6626 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw6627 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw6627step0 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw6627step1 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw6627step2 line 73
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6627 line 75
  17. def OAI.MUB6.Certificate.PairSemantics.raw6628 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw6628step0 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw6628step1 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw6628step2 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6628 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw6629 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw6629step0 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw6629step1 line 121
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6629 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw6630 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw6630step0 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw6630step1 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw6630step2 line 142
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6630 line 144
  31. def OAI.MUB6.Certificate.PairSemantics.raw6631 line 161
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6631 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw6632 line 167
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6632 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw6633 line 173
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6633 line 175
  37. def OAI.MUB6.Certificate.PairSemantics.raw6634 line 179
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6634 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw6635 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw6635step0 line 187
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6635 line 189
  42. def OAI.MUB6.Certificate.PairSemantics.raw6636 line 198
  43. def OAI.MUB6.Certificate.PairSemantics.raw6636step0 line 200
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6636 line 202
  45. def OAI.MUB6.Certificate.PairSemantics.raw6637 line 211
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6637 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw6638 line 217
  48. def OAI.MUB6.Certificate.PairSemantics.raw6638step0 line 219
  49. def OAI.MUB6.Certificate.PairSemantics.raw6638step1 line 221
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6638 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw6639 line 236
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6639 line 238
  53. def OAI.MUB6.Certificate.PairSemantics.raw6640 line 242
  54. def OAI.MUB6.Certificate.PairSemantics.raw6640step0 line 244
  55. def OAI.MUB6.Certificate.PairSemantics.raw6640step1 line 246
  56. def OAI.MUB6.Certificate.PairSemantics.raw6640step2 line 248
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6640 line 250
  58. def OAI.MUB6.Certificate.PairSemantics.raw6641 line 267
  59. def OAI.MUB6.Certificate.PairSemantics.raw6641step0 line 269
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6641 line 271
  61. def OAI.MUB6.Certificate.PairSemantics.raw6642 line 280
  62. def OAI.MUB6.Certificate.PairSemantics.raw6642step0 line 282
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6642 line 284
  64. def OAI.MUB6.Certificate.PairSemantics.raw6643 line 293
  65. def OAI.MUB6.Certificate.PairSemantics.raw6643step0 line 295
  66. def OAI.MUB6.Certificate.PairSemantics.raw6643step1 line 297
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6643 line 299
  68. def OAI.MUB6.Certificate.PairSemantics.raw6644 line 312
  69. def OAI.MUB6.Certificate.PairSemantics.raw6644step0 line 314
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6644 line 316
  71. def OAI.MUB6.Certificate.PairSemantics.raw6645 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6645 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw6646 line 331
  74. def OAI.MUB6.Certificate.PairSemantics.raw6646step0 line 333
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6646 line 335
  76. def OAI.MUB6.Certificate.PairSemantics.raw6647 line 344
  77. def OAI.MUB6.Certificate.PairSemantics.raw6647step0 line 346
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6647 line 348
  79. def OAI.MUB6.Certificate.PairSemantics.raw6648 line 357
  80. def OAI.MUB6.Certificate.PairSemantics.raw6648step0 line 359
  81. def OAI.MUB6.Certificate.PairSemantics.raw6648step1 line 361
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6648 line 363
  83. def OAI.MUB6.Certificate.PairSemantics.raw6649 line 376
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6649 line 378
  85. def OAI.MUB6.Certificate.PairSemantics.raw6650 line 382
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6650 line 384
  87. def OAI.MUB6.Certificate.PairSemantics.raw6651 line 388
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6651 line 390
  89. def OAI.MUB6.Certificate.PairSemantics.raw6652 line 394
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6652 line 396
  91. def OAI.MUB6.Certificate.PairSemantics.raw6653 line 400
  92. def OAI.MUB6.Certificate.PairSemantics.raw6653step0 line 402
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6653 line 404
  94. def OAI.MUB6.Certificate.PairSemantics.raw6654 line 413
  95. def OAI.MUB6.Certificate.PairSemantics.raw6654step0 line 415
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical6654 line 417
  97. def OAI.MUB6.Certificate.PairSemantics.raw6655 line 426
  98. def OAI.MUB6.Certificate.PairSemantics.raw6655step0 line 428
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6655 line 430