OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical159.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5088 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw5088step0 line 23
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5088 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw5089 line 34
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5089 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw5090 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw5090step0 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5090 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw5091 line 53
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical5091 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw5092 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw5092step0 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw5092step1 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw5092step2 line 65
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5092 line 67
  16. def OAI.MUB6.Certificate.PairSemantics.raw5093 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw5093step0 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw5093step1 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw5093step2 line 90
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5093 line 92
  21. def OAI.MUB6.Certificate.PairSemantics.raw5094 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw5094step0 line 111
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5094 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw5095 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw5095step0 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw5095step1 line 126
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5095 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw5096 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw5096step0 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw5096step1 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw5096step2 line 147
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5096 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw5097 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw5097step0 line 168
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5097 line 170
  36. def OAI.MUB6.Certificate.PairSemantics.raw5098 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw5098step0 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw5098step1 line 183
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5098 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw5099 line 198
  41. def OAI.MUB6.Certificate.PairSemantics.raw5099step0 line 200
  42. def OAI.MUB6.Certificate.PairSemantics.raw5099step1 line 202
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5099 line 204
  44. def OAI.MUB6.Certificate.PairSemantics.raw5100 line 217
  45. def OAI.MUB6.Certificate.PairSemantics.raw5100step0 line 219
  46. def OAI.MUB6.Certificate.PairSemantics.raw5100step1 line 221
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5100 line 223
  48. def OAI.MUB6.Certificate.PairSemantics.raw5101 line 236
  49. def OAI.MUB6.Certificate.PairSemantics.raw5101step0 line 238
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical5101 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw5102 line 249
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5102 line 251
  53. def OAI.MUB6.Certificate.PairSemantics.raw5103 line 255
  54. def OAI.MUB6.Certificate.PairSemantics.raw5103step0 line 257
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5103 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw5104 line 268
  57. def OAI.MUB6.Certificate.PairSemantics.raw5104step0 line 270
  58. def OAI.MUB6.Certificate.PairSemantics.raw5104step1 line 272
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5104 line 274
  60. def OAI.MUB6.Certificate.PairSemantics.raw5105 line 289
  61. def OAI.MUB6.Certificate.PairSemantics.raw5105step0 line 291
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5105 line 293
  63. def OAI.MUB6.Certificate.PairSemantics.raw5106 line 303
  64. def OAI.MUB6.Certificate.PairSemantics.raw5106step0 line 305
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5106 line 307
  66. def OAI.MUB6.Certificate.PairSemantics.raw5107 line 317
  67. def OAI.MUB6.Certificate.PairSemantics.raw5107step0 line 319
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5107 line 321
  69. def OAI.MUB6.Certificate.PairSemantics.raw5108 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw5108step0 line 333
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5108 line 335
  72. def OAI.MUB6.Certificate.PairSemantics.raw5109 line 345
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5109 line 347
  74. def OAI.MUB6.Certificate.PairSemantics.raw5110 line 351
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5110 line 353
  76. def OAI.MUB6.Certificate.PairSemantics.raw5111 line 357
  77. def OAI.MUB6.Certificate.PairSemantics.raw5111step0 line 359
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5111 line 361
  79. def OAI.MUB6.Certificate.PairSemantics.raw5112 line 370
  80. def OAI.MUB6.Certificate.PairSemantics.raw5112step0 line 372
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5112 line 374
  82. def OAI.MUB6.Certificate.PairSemantics.raw5113 line 383
  83. def OAI.MUB6.Certificate.PairSemantics.raw5113step0 line 385
  84. def OAI.MUB6.Certificate.PairSemantics.raw5113step1 line 387
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5113 line 389
  86. def OAI.MUB6.Certificate.PairSemantics.raw5114 line 403
  87. def OAI.MUB6.Certificate.PairSemantics.raw5114step0 line 405
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5114 line 407
  89. def OAI.MUB6.Certificate.PairSemantics.raw5115 line 417
  90. def OAI.MUB6.Certificate.PairSemantics.raw5115step0 line 419
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5115 line 421
  92. def OAI.MUB6.Certificate.PairSemantics.raw5116 line 430
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5116 line 432
  94. def OAI.MUB6.Certificate.PairSemantics.raw5117 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw5117step0 line 438
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical5117 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw5118 line 449
  98. def OAI.MUB6.Certificate.PairSemantics.raw5118step0 line 451
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5118 line 453
  100. def OAI.MUB6.Certificate.PairSemantics.raw5119 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw5119step0 line 464
  102. def OAI.MUB6.Certificate.PairSemantics.raw5119step1 line 466
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5119 line 468