OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical208.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6656 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical6656 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw6657 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6657 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw6658 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6658 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw6659 line 36
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6659 line 38
  9. def OAI.MUB6.Certificate.PairSemantics.raw6660 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw6660step0 line 44
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6660 line 46
  12. def OAI.MUB6.Certificate.PairSemantics.raw6661 line 55
  13. def OAI.MUB6.Certificate.PairSemantics.raw6661step0 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw6661step1 line 59
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6661 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw6662 line 74
  17. def OAI.MUB6.Certificate.PairSemantics.raw6662step0 line 76
  18. def OAI.MUB6.Certificate.PairSemantics.raw6662step1 line 78
  19. def OAI.MUB6.Certificate.PairSemantics.raw6662step2 line 80
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6662 line 82
  21. def OAI.MUB6.Certificate.PairSemantics.raw6663 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw6663step0 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw6663step1 line 103
  24. def OAI.MUB6.Certificate.PairSemantics.raw6663step2 line 105
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6663 line 107
  26. def OAI.MUB6.Certificate.PairSemantics.raw6664 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw6664step0 line 126
  28. def OAI.MUB6.Certificate.PairSemantics.raw6664step1 line 128
  29. def OAI.MUB6.Certificate.PairSemantics.raw6664step2 line 130
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6664 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw6665 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw6665step0 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw6665step1 line 154
  34. def OAI.MUB6.Certificate.PairSemantics.raw6665step2 line 156
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6665 line 158
  36. def OAI.MUB6.Certificate.PairSemantics.raw6666 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw6666step0 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw6666step1 line 180
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6666 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw6667 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw6667step0 line 198
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6667 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw6668 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw6668step0 line 211
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6668 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw6669 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw6669step0 line 224
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6669 line 226
  49. def OAI.MUB6.Certificate.PairSemantics.raw6670 line 235
  50. def OAI.MUB6.Certificate.PairSemantics.raw6670step0 line 237
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6670 line 239
  52. def OAI.MUB6.Certificate.PairSemantics.raw6671 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw6671step0 line 250
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6671 line 252
  55. def OAI.MUB6.Certificate.PairSemantics.raw6672 line 261
  56. def OAI.MUB6.Certificate.PairSemantics.raw6672step0 line 263
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6672 line 265
  58. def OAI.MUB6.Certificate.PairSemantics.raw6673 line 274
  59. def OAI.MUB6.Certificate.PairSemantics.raw6673step0 line 276
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6673 line 278
  61. def OAI.MUB6.Certificate.PairSemantics.raw6674 line 287
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6674 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw6675 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw6675step0 line 295
  65. def OAI.MUB6.Certificate.PairSemantics.raw6675step1 line 297
  66. def OAI.MUB6.Certificate.PairSemantics.raw6675step2 line 299
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6675 line 301
  68. def OAI.MUB6.Certificate.PairSemantics.raw6676 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw6676step0 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw6676step1 line 322
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6676 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw6677 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw6677step0 line 339
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6677 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw6678 line 350
  76. def OAI.MUB6.Certificate.PairSemantics.raw6678step0 line 352
  77. def OAI.MUB6.Certificate.PairSemantics.raw6678step1 line 354
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6678 line 356
  79. def OAI.MUB6.Certificate.PairSemantics.raw6679 line 369
  80. def OAI.MUB6.Certificate.PairSemantics.raw6679step0 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw6679step1 line 373
  82. def OAI.MUB6.Certificate.PairSemantics.raw6679step2 line 375
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6679 line 377
  84. def OAI.MUB6.Certificate.PairSemantics.raw6680 line 394
  85. def OAI.MUB6.Certificate.PairSemantics.raw6680step0 line 396
  86. def OAI.MUB6.Certificate.PairSemantics.raw6680step1 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw6680step2 line 400
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6680 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw6681 line 419
  90. def OAI.MUB6.Certificate.PairSemantics.raw6681step0 line 421
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6681 line 423
  92. def OAI.MUB6.Certificate.PairSemantics.raw6682 line 432
  93. def OAI.MUB6.Certificate.PairSemantics.raw6682step0 line 434
  94. def OAI.MUB6.Certificate.PairSemantics.raw6682step1 line 436
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6682 line 438
  96. def OAI.MUB6.Certificate.PairSemantics.raw6683 line 451
  97. def OAI.MUB6.Certificate.PairSemantics.raw6683step0 line 453
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical6683 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw6684 line 464
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical6684 line 466
  101. def OAI.MUB6.Certificate.PairSemantics.raw6685 line 470
  102. def OAI.MUB6.Certificate.PairSemantics.raw6685step0 line 472
  103. def OAI.MUB6.Certificate.PairSemantics.raw6685step1 line 474
  104. def OAI.MUB6.Certificate.PairSemantics.raw6685step2 line 476
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical6685 line 478
  106. def OAI.MUB6.Certificate.PairSemantics.raw6686 line 495
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical6686 line 497
  108. def OAI.MUB6.Certificate.PairSemantics.raw6687 line 501
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical6687 line 503