OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical244.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7808 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw7808step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw7808step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7808 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw7809 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw7809step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw7809step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7809 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw7810 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw7810step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw7810step1 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7810 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw7811 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw7811step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw7811step1 line 81
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7811 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw7812 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw7812step0 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw7812step1 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7812 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw7813 line 115
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7813 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw7814 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw7814step0 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw7814step1 line 125
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7814 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw7815 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw7815step0 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw7815step1 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7815 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw7816 line 159
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7816 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw7817 line 165
  34. def OAI.MUB6.Certificate.PairSemantics.raw7817step0 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw7817step1 line 169
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7817 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw7818 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw7818step0 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw7818step1 line 188
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7818 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw7819 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw7819step0 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw7819step1 line 207
  44. def OAI.MUB6.Certificate.PairSemantics.raw7819step2 line 209
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7819 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw7820 line 228
  47. def OAI.MUB6.Certificate.PairSemantics.raw7820step0 line 230
  48. def OAI.MUB6.Certificate.PairSemantics.raw7820step1 line 232
  49. def OAI.MUB6.Certificate.PairSemantics.raw7820step2 line 234
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7820 line 236
  51. def OAI.MUB6.Certificate.PairSemantics.raw7821 line 253
  52. def OAI.MUB6.Certificate.PairSemantics.raw7821step0 line 255
  53. def OAI.MUB6.Certificate.PairSemantics.raw7821step1 line 257
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7821 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw7822 line 272
  56. def OAI.MUB6.Certificate.PairSemantics.raw7822step0 line 274
  57. def OAI.MUB6.Certificate.PairSemantics.raw7822step1 line 276
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical7822 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw7823 line 291
  60. def OAI.MUB6.Certificate.PairSemantics.raw7823step0 line 293
  61. def OAI.MUB6.Certificate.PairSemantics.raw7823step1 line 295
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7823 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw7824 line 310
  64. def OAI.MUB6.Certificate.PairSemantics.raw7824step0 line 312
  65. def OAI.MUB6.Certificate.PairSemantics.raw7824step1 line 314
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7824 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw7825 line 329
  68. def OAI.MUB6.Certificate.PairSemantics.raw7825step0 line 331
  69. def OAI.MUB6.Certificate.PairSemantics.raw7825step1 line 333
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7825 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw7826 line 348
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7826 line 350
  73. def OAI.MUB6.Certificate.PairSemantics.raw7827 line 354
  74. def OAI.MUB6.Certificate.PairSemantics.raw7827step0 line 356
  75. def OAI.MUB6.Certificate.PairSemantics.raw7827step1 line 358
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7827 line 360
  77. def OAI.MUB6.Certificate.PairSemantics.raw7828 line 373
  78. def OAI.MUB6.Certificate.PairSemantics.raw7828step0 line 375
  79. def OAI.MUB6.Certificate.PairSemantics.raw7828step1 line 377
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7828 line 379
  81. def OAI.MUB6.Certificate.PairSemantics.raw7829 line 392
  82. def OAI.MUB6.Certificate.PairSemantics.raw7829step0 line 394
  83. def OAI.MUB6.Certificate.PairSemantics.raw7829step1 line 396
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7829 line 398
  85. def OAI.MUB6.Certificate.PairSemantics.raw7830 line 411
  86. def OAI.MUB6.Certificate.PairSemantics.raw7830step0 line 413
  87. def OAI.MUB6.Certificate.PairSemantics.raw7830step1 line 415
  88. def OAI.MUB6.Certificate.PairSemantics.raw7830step2 line 417
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7830 line 419
  90. def OAI.MUB6.Certificate.PairSemantics.raw7831 line 436
  91. def OAI.MUB6.Certificate.PairSemantics.raw7831step0 line 438
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7831 line 440
  93. def OAI.MUB6.Certificate.PairSemantics.raw7832 line 449
  94. def OAI.MUB6.Certificate.PairSemantics.raw7832step0 line 451
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7832 line 453
  96. def OAI.MUB6.Certificate.PairSemantics.raw7833 line 462
  97. def OAI.MUB6.Certificate.PairSemantics.raw7833step0 line 464
  98. def OAI.MUB6.Certificate.PairSemantics.raw7833step1 line 466
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7833 line 468
  100. def OAI.MUB6.Certificate.PairSemantics.raw7834 line 481
  101. def OAI.MUB6.Certificate.PairSemantics.raw7834step0 line 483
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical7834 line 485
  103. def OAI.MUB6.Certificate.PairSemantics.raw7835 line 494
  104. def OAI.MUB6.Certificate.PairSemantics.raw7835step0 line 496
  105. def OAI.MUB6.Certificate.PairSemantics.raw7835step1 line 498
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical7835 line 500
  107. def OAI.MUB6.Certificate.PairSemantics.raw7836 line 513
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7836 line 515
  109. def OAI.MUB6.Certificate.PairSemantics.raw7837 line 519
  110. def OAI.MUB6.Certificate.PairSemantics.raw7837step0 line 521
  111. def OAI.MUB6.Certificate.PairSemantics.raw7837step1 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw7837step2 line 525
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7837 line 527
  114. def OAI.MUB6.Certificate.PairSemantics.raw7838 line 544
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical7838 line 546
  116. def OAI.MUB6.Certificate.PairSemantics.raw7839 line 550
  117. def OAI.MUB6.Certificate.PairSemantics.raw7839step0 line 552
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7839 line 554