OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical231.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7392 line 19
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical7392 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw7393 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw7393step0 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw7393step1 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical7393 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw7394 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw7394step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7394 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw7395 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw7395step0 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw7395step1 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7395 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw7396 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw7396step0 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7396 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw7397 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw7397step0 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw7397step1 line 93
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7397 line 95
  21. def OAI.MUB6.Certificate.PairSemantics.raw7398 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw7398step0 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7398 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw7399 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw7399step0 line 123
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7399 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw7400 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw7400step0 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw7400step1 line 138
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7400 line 140
  31. def OAI.MUB6.Certificate.PairSemantics.raw7401 line 153
  32. def OAI.MUB6.Certificate.PairSemantics.raw7401step0 line 155
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7401 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw7402 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw7402step0 line 168
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7402 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw7403 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw7403step0 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw7403step1 line 183
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7403 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw7404 line 198
  42. def OAI.MUB6.Certificate.PairSemantics.raw7404step0 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw7404step1 line 202
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7404 line 204
  45. def OAI.MUB6.Certificate.PairSemantics.raw7405 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw7405step0 line 219
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical7405 line 221
  48. def OAI.MUB6.Certificate.PairSemantics.raw7406 line 231
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical7406 line 233
  50. def OAI.MUB6.Certificate.PairSemantics.raw7407 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw7407step0 line 239
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7407 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw7408 line 251
  54. def OAI.MUB6.Certificate.PairSemantics.raw7408step0 line 253
  55. def OAI.MUB6.Certificate.PairSemantics.raw7408step1 line 255
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical7408 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw7409 line 270
  58. def OAI.MUB6.Certificate.PairSemantics.raw7409step0 line 272
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7409 line 274
  60. def OAI.MUB6.Certificate.PairSemantics.raw7410 line 283
  61. def OAI.MUB6.Certificate.PairSemantics.raw7410step0 line 285
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7410 line 287
  63. def OAI.MUB6.Certificate.PairSemantics.raw7411 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw7411step0 line 298
  65. def OAI.MUB6.Certificate.PairSemantics.raw7411step1 line 300
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7411 line 302
  67. def OAI.MUB6.Certificate.PairSemantics.raw7412 line 315
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical7412 line 317
  69. def OAI.MUB6.Certificate.PairSemantics.raw7413 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw7413step0 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw7413step1 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7413 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw7414 line 340
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7414 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw7415 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw7415step0 line 348
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical7415 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw7416 line 360
  79. def OAI.MUB6.Certificate.PairSemantics.raw7416step0 line 362
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7416 line 364
  81. def OAI.MUB6.Certificate.PairSemantics.raw7417 line 373
  82. def OAI.MUB6.Certificate.PairSemantics.raw7417step0 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw7417step1 line 377
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7417 line 379
  85. def OAI.MUB6.Certificate.PairSemantics.raw7418 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw7418step0 line 394
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7418 line 396
  88. def OAI.MUB6.Certificate.PairSemantics.raw7419 line 405
  89. def OAI.MUB6.Certificate.PairSemantics.raw7419step0 line 407
  90. def OAI.MUB6.Certificate.PairSemantics.raw7419step1 line 409
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7419 line 411
  92. def OAI.MUB6.Certificate.PairSemantics.raw7420 line 424
  93. def OAI.MUB6.Certificate.PairSemantics.raw7420step0 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw7420step1 line 428
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7420 line 430
  96. def OAI.MUB6.Certificate.PairSemantics.raw7421 line 443
  97. def OAI.MUB6.Certificate.PairSemantics.raw7421step0 line 445
  98. def OAI.MUB6.Certificate.PairSemantics.raw7421step1 line 447
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7421 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw7422 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw7422step0 line 464
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical7422 line 466
  103. def OAI.MUB6.Certificate.PairSemantics.raw7423 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw7423step0 line 477
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7423 line 479