OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical246.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7872 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw7872step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw7872step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7872 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw7873 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw7873step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw7873step1 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw7873step2 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7873 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw7874 line 64
  11. def OAI.MUB6.Certificate.PairSemantics.raw7874step0 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw7874step1 line 68
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7874 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw7875 line 83
  15. def OAI.MUB6.Certificate.PairSemantics.raw7875step0 line 85
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7875 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw7876 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw7876step0 line 98
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7876 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw7877 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw7877step0 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw7877step1 line 113
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7877 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw7878 line 128
  25. def OAI.MUB6.Certificate.PairSemantics.raw7878step0 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw7878step1 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7878 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw7879 line 147
  29. def OAI.MUB6.Certificate.PairSemantics.raw7879step0 line 149
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7879 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw7880 line 160
  32. def OAI.MUB6.Certificate.PairSemantics.raw7880step0 line 162
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7880 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw7881 line 173
  35. def OAI.MUB6.Certificate.PairSemantics.raw7881step0 line 175
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7881 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw7882 line 186
  38. def OAI.MUB6.Certificate.PairSemantics.raw7882step0 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw7882step1 line 190
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7882 line 192
  41. def OAI.MUB6.Certificate.PairSemantics.raw7883 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw7883step0 line 208
  43. def OAI.MUB6.Certificate.PairSemantics.raw7883step1 line 210
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7883 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw7884 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw7884step0 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw7884step1 line 229
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7884 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw7885 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw7885step0 line 246
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical7885 line 248
  52. def OAI.MUB6.Certificate.PairSemantics.raw7886 line 257
  53. def OAI.MUB6.Certificate.PairSemantics.raw7886step0 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw7886step1 line 261
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7886 line 263
  56. def OAI.MUB6.Certificate.PairSemantics.raw7887 line 277
  57. def OAI.MUB6.Certificate.PairSemantics.raw7887step0 line 279
  58. def OAI.MUB6.Certificate.PairSemantics.raw7887step1 line 281
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7887 line 283
  60. def OAI.MUB6.Certificate.PairSemantics.raw7888 line 296
  61. def OAI.MUB6.Certificate.PairSemantics.raw7888step0 line 298
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7888 line 300
  63. def OAI.MUB6.Certificate.PairSemantics.raw7889 line 309
  64. def OAI.MUB6.Certificate.PairSemantics.raw7889step0 line 311
  65. def OAI.MUB6.Certificate.PairSemantics.raw7889step1 line 313
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7889 line 315
  67. def OAI.MUB6.Certificate.PairSemantics.raw7890 line 328
  68. def OAI.MUB6.Certificate.PairSemantics.raw7890step0 line 330
  69. def OAI.MUB6.Certificate.PairSemantics.raw7890step1 line 332
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7890 line 334
  71. def OAI.MUB6.Certificate.PairSemantics.raw7891 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw7891step0 line 349
  73. def OAI.MUB6.Certificate.PairSemantics.raw7891step1 line 351
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7891 line 353
  75. def OAI.MUB6.Certificate.PairSemantics.raw7892 line 366
  76. def OAI.MUB6.Certificate.PairSemantics.raw7892step0 line 368
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical7892 line 370
  78. def OAI.MUB6.Certificate.PairSemantics.raw7893 line 379
  79. def OAI.MUB6.Certificate.PairSemantics.raw7893step0 line 381
  80. def OAI.MUB6.Certificate.PairSemantics.raw7893step1 line 383
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical7893 line 385
  82. def OAI.MUB6.Certificate.PairSemantics.raw7894 line 399
  83. def OAI.MUB6.Certificate.PairSemantics.raw7894step0 line 401
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7894 line 403
  85. def OAI.MUB6.Certificate.PairSemantics.raw7895 line 412
  86. def OAI.MUB6.Certificate.PairSemantics.raw7895step0 line 414
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7895 line 416
  88. def OAI.MUB6.Certificate.PairSemantics.raw7896 line 426
  89. def OAI.MUB6.Certificate.PairSemantics.raw7896step0 line 428
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical7896 line 430
  91. def OAI.MUB6.Certificate.PairSemantics.raw7897 line 439
  92. def OAI.MUB6.Certificate.PairSemantics.raw7897step0 line 441
  93. def OAI.MUB6.Certificate.PairSemantics.raw7897step1 line 443
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7897 line 445
  95. def OAI.MUB6.Certificate.PairSemantics.raw7898 line 458
  96. def OAI.MUB6.Certificate.PairSemantics.raw7898step0 line 460
  97. def OAI.MUB6.Certificate.PairSemantics.raw7898step1 line 462
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7898 line 464
  99. def OAI.MUB6.Certificate.PairSemantics.raw7899 line 477
  100. def OAI.MUB6.Certificate.PairSemantics.raw7899step0 line 479
  101. def OAI.MUB6.Certificate.PairSemantics.raw7899step1 line 481
  102. def OAI.MUB6.Certificate.PairSemantics.raw7899step2 line 483
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7899 line 485
  104. def OAI.MUB6.Certificate.PairSemantics.raw7900 line 502
  105. def OAI.MUB6.Certificate.PairSemantics.raw7900step0 line 504
  106. def OAI.MUB6.Certificate.PairSemantics.raw7900step1 line 506
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7900 line 508
  108. def OAI.MUB6.Certificate.PairSemantics.raw7901 line 521
  109. def OAI.MUB6.Certificate.PairSemantics.raw7901step0 line 523
  110. def OAI.MUB6.Certificate.PairSemantics.raw7901step1 line 525
  111. def OAI.MUB6.Certificate.PairSemantics.raw7901step2 line 527
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7901 line 529
  113. def OAI.MUB6.Certificate.PairSemantics.raw7902 line 546
  114. def OAI.MUB6.Certificate.PairSemantics.raw7902step0 line 548
  115. def OAI.MUB6.Certificate.PairSemantics.raw7902step1 line 550
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7902 line 552
  117. def OAI.MUB6.Certificate.PairSemantics.raw7903 line 565
  118. def OAI.MUB6.Certificate.PairSemantics.raw7903step0 line 567
  119. def OAI.MUB6.Certificate.PairSemantics.raw7903step1 line 569
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical7903 line 571