OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical175.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5600 line 17
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5600 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw5601 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw5601step0 line 25
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5601 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw5602 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw5602step0 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw5602step1 line 40
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5602 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw5603 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw5603step0 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw5603step1 line 59
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5603 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw5604 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw5604step0 line 76
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5604 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw5605 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw5605step0 line 89
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5605 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw5606 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw5606step0 line 102
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5606 line 104
  23. def OAI.MUB6.Certificate.PairSemantics.raw5607 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw5607step0 line 115
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5607 line 117
  26. def OAI.MUB6.Certificate.PairSemantics.raw5608 line 126
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5608 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw5609 line 132
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5609 line 134
  30. def OAI.MUB6.Certificate.PairSemantics.raw5610 line 138
  31. def OAI.MUB6.Certificate.PairSemantics.raw5610step0 line 140
  32. def OAI.MUB6.Certificate.PairSemantics.raw5610step1 line 142
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5610 line 144
  34. def OAI.MUB6.Certificate.PairSemantics.raw5611 line 157
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5611 line 159
  36. def OAI.MUB6.Certificate.PairSemantics.raw5612 line 163
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical5612 line 165
  38. def OAI.MUB6.Certificate.PairSemantics.raw5613 line 169
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5613 line 171
  40. def OAI.MUB6.Certificate.PairSemantics.raw5614 line 175
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5614 line 177
  42. def OAI.MUB6.Certificate.PairSemantics.raw5615 line 181
  43. def OAI.MUB6.Certificate.PairSemantics.raw5615step0 line 183
  44. def OAI.MUB6.Certificate.PairSemantics.raw5615step1 line 185
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5615 line 187
  46. def OAI.MUB6.Certificate.PairSemantics.raw5616 line 200
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5616 line 202
  48. def OAI.MUB6.Certificate.PairSemantics.raw5617 line 206
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5617 line 208
  50. def OAI.MUB6.Certificate.PairSemantics.raw5618 line 212
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5618 line 214
  52. def OAI.MUB6.Certificate.PairSemantics.raw5619 line 218
  53. def OAI.MUB6.Certificate.PairSemantics.raw5619step0 line 220
  54. def OAI.MUB6.Certificate.PairSemantics.raw5619step1 line 222
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5619 line 224
  56. def OAI.MUB6.Certificate.PairSemantics.raw5620 line 237
  57. def OAI.MUB6.Certificate.PairSemantics.raw5620step0 line 239
  58. def OAI.MUB6.Certificate.PairSemantics.raw5620step1 line 241
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5620 line 243
  60. def OAI.MUB6.Certificate.PairSemantics.raw5621 line 256
  61. def OAI.MUB6.Certificate.PairSemantics.raw5621step0 line 258
  62. def OAI.MUB6.Certificate.PairSemantics.raw5621step1 line 260
  63. def OAI.MUB6.Certificate.PairSemantics.raw5621step2 line 262
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5621 line 264
  65. def OAI.MUB6.Certificate.PairSemantics.raw5622 line 281
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5622 line 283
  67. def OAI.MUB6.Certificate.PairSemantics.raw5623 line 287
  68. def OAI.MUB6.Certificate.PairSemantics.raw5623step0 line 289
  69. def OAI.MUB6.Certificate.PairSemantics.raw5623step1 line 291
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical5623 line 293
  71. def OAI.MUB6.Certificate.PairSemantics.raw5624 line 306
  72. def OAI.MUB6.Certificate.PairSemantics.raw5624step0 line 308
  73. def OAI.MUB6.Certificate.PairSemantics.raw5624step1 line 310
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5624 line 312
  75. def OAI.MUB6.Certificate.PairSemantics.raw5625 line 325
  76. def OAI.MUB6.Certificate.PairSemantics.raw5625step0 line 327
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5625 line 329
  78. def OAI.MUB6.Certificate.PairSemantics.raw5626 line 338
  79. def OAI.MUB6.Certificate.PairSemantics.raw5626step0 line 340
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5626 line 342
  81. def OAI.MUB6.Certificate.PairSemantics.raw5627 line 351
  82. def OAI.MUB6.Certificate.PairSemantics.raw5627step0 line 353
  83. def OAI.MUB6.Certificate.PairSemantics.raw5627step1 line 355
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5627 line 357
  85. def OAI.MUB6.Certificate.PairSemantics.raw5628 line 370
  86. def OAI.MUB6.Certificate.PairSemantics.raw5628step0 line 372
  87. def OAI.MUB6.Certificate.PairSemantics.raw5628step1 line 374
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5628 line 376
  89. def OAI.MUB6.Certificate.PairSemantics.raw5629 line 389
  90. def OAI.MUB6.Certificate.PairSemantics.raw5629step0 line 391
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5629 line 393
  92. def OAI.MUB6.Certificate.PairSemantics.raw5630 line 402
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5630 line 404
  94. def OAI.MUB6.Certificate.PairSemantics.raw5631 line 408
  95. def OAI.MUB6.Certificate.PairSemantics.raw5631step0 line 410
  96. def OAI.MUB6.Certificate.PairSemantics.raw5631step1 line 412
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5631 line 414