OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical177.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5664 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw5664step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw5664step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5664 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw5665 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw5665step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw5665step1 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw5665step2 line 41
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5665 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw5666 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw5666step0 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw5666step1 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw5666step2 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5666 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw5667 line 87
  16. def OAI.MUB6.Certificate.PairSemantics.raw5667step0 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw5667step1 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw5667step2 line 93
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5667 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw5668 line 113
  21. def OAI.MUB6.Certificate.PairSemantics.raw5668step0 line 115
  22. def OAI.MUB6.Certificate.PairSemantics.raw5668step1 line 117
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5668 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw5669 line 133
  25. def OAI.MUB6.Certificate.PairSemantics.raw5669step0 line 135
  26. def OAI.MUB6.Certificate.PairSemantics.raw5669step1 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw5669step2 line 139
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5669 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw5670 line 159
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5670 line 161
  31. def OAI.MUB6.Certificate.PairSemantics.raw5671 line 165
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5671 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw5672 line 171
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical5672 line 173
  35. def OAI.MUB6.Certificate.PairSemantics.raw5673 line 177
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5673 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw5674 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw5674step0 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw5674step1 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5674 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw5675 line 202
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5675 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw5676 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw5676step0 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5676 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw5677 line 221
  47. def OAI.MUB6.Certificate.PairSemantics.raw5677step0 line 223
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5677 line 225
  49. def OAI.MUB6.Certificate.PairSemantics.raw5678 line 234
  50. def OAI.MUB6.Certificate.PairSemantics.raw5678step0 line 236
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5678 line 238
  52. def OAI.MUB6.Certificate.PairSemantics.raw5679 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw5679step0 line 249
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5679 line 251
  55. def OAI.MUB6.Certificate.PairSemantics.raw5680 line 260
  56. def OAI.MUB6.Certificate.PairSemantics.raw5680step0 line 262
  57. def OAI.MUB6.Certificate.PairSemantics.raw5680step1 line 264
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5680 line 266
  59. def OAI.MUB6.Certificate.PairSemantics.raw5681 line 279
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5681 line 281
  61. def OAI.MUB6.Certificate.PairSemantics.raw5682 line 285
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5682 line 287
  63. def OAI.MUB6.Certificate.PairSemantics.raw5683 line 291
  64. def OAI.MUB6.Certificate.PairSemantics.raw5683step0 line 293
  65. def OAI.MUB6.Certificate.PairSemantics.raw5683step1 line 295
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5683 line 297
  67. def OAI.MUB6.Certificate.PairSemantics.raw5684 line 310
  68. def OAI.MUB6.Certificate.PairSemantics.raw5684step0 line 312
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5684 line 314
  70. def OAI.MUB6.Certificate.PairSemantics.raw5685 line 323
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5685 line 325
  72. def OAI.MUB6.Certificate.PairSemantics.raw5686 line 329
  73. def OAI.MUB6.Certificate.PairSemantics.raw5686step0 line 331
  74. def OAI.MUB6.Certificate.PairSemantics.raw5686step1 line 333
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5686 line 335
  76. def OAI.MUB6.Certificate.PairSemantics.raw5687 line 348
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5687 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw5688 line 354
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5688 line 356
  80. def OAI.MUB6.Certificate.PairSemantics.raw5689 line 360
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5689 line 362
  82. def OAI.MUB6.Certificate.PairSemantics.raw5690 line 366
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5690 line 368
  84. def OAI.MUB6.Certificate.PairSemantics.raw5691 line 372
  85. def OAI.MUB6.Certificate.PairSemantics.raw5691step0 line 374
  86. def OAI.MUB6.Certificate.PairSemantics.raw5691step1 line 376
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5691 line 378
  88. def OAI.MUB6.Certificate.PairSemantics.raw5692 line 391
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5692 line 393
  90. def OAI.MUB6.Certificate.PairSemantics.raw5693 line 397
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5693 line 399
  92. def OAI.MUB6.Certificate.PairSemantics.raw5694 line 403
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5694 line 405
  94. def OAI.MUB6.Certificate.PairSemantics.raw5695 line 409
  95. def OAI.MUB6.Certificate.PairSemantics.raw5695step0 line 411
  96. def OAI.MUB6.Certificate.PairSemantics.raw5695step1 line 413
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5695 line 415