OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical217.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6944 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw6944step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw6944step1 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw6944step2 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6944 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw6945 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw6945step0 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw6945step1 line 47
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6945 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw6946 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw6946step0 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw6946step1 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw6946step2 line 68
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6946 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw6947 line 87
  16. def OAI.MUB6.Certificate.PairSemantics.raw6947step0 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw6947step1 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw6947step2 line 93
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6947 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw6948 line 112
  21. def OAI.MUB6.Certificate.PairSemantics.raw6948step0 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw6948step1 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw6948step2 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6948 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw6949 line 137
  26. def OAI.MUB6.Certificate.PairSemantics.raw6949step0 line 139
  27. def OAI.MUB6.Certificate.PairSemantics.raw6949step1 line 141
  28. def OAI.MUB6.Certificate.PairSemantics.raw6949step2 line 143
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6949 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw6950 line 162
  31. def OAI.MUB6.Certificate.PairSemantics.raw6950step0 line 164
  32. def OAI.MUB6.Certificate.PairSemantics.raw6950step1 line 166
  33. def OAI.MUB6.Certificate.PairSemantics.raw6950step2 line 168
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6950 line 170
  35. def OAI.MUB6.Certificate.PairSemantics.raw6951 line 187
  36. def OAI.MUB6.Certificate.PairSemantics.raw6951step0 line 189
  37. def OAI.MUB6.Certificate.PairSemantics.raw6951step1 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw6951step2 line 193
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6951 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw6952 line 212
  41. def OAI.MUB6.Certificate.PairSemantics.raw6952step0 line 214
  42. def OAI.MUB6.Certificate.PairSemantics.raw6952step1 line 216
  43. def OAI.MUB6.Certificate.PairSemantics.raw6952step2 line 218
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6952 line 220
  45. def OAI.MUB6.Certificate.PairSemantics.raw6953 line 237
  46. def OAI.MUB6.Certificate.PairSemantics.raw6953step0 line 239
  47. def OAI.MUB6.Certificate.PairSemantics.raw6953step1 line 241
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6953 line 243
  49. def OAI.MUB6.Certificate.PairSemantics.raw6954 line 256
  50. def OAI.MUB6.Certificate.PairSemantics.raw6954step0 line 258
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6954 line 260
  52. def OAI.MUB6.Certificate.PairSemantics.raw6955 line 269
  53. def OAI.MUB6.Certificate.PairSemantics.raw6955step0 line 271
  54. def OAI.MUB6.Certificate.PairSemantics.raw6955step1 line 273
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6955 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw6956 line 288
  57. def OAI.MUB6.Certificate.PairSemantics.raw6956step0 line 290
  58. def OAI.MUB6.Certificate.PairSemantics.raw6956step1 line 292
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6956 line 294
  60. def OAI.MUB6.Certificate.PairSemantics.raw6957 line 307
  61. def OAI.MUB6.Certificate.PairSemantics.raw6957step0 line 309
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6957 line 311
  63. def OAI.MUB6.Certificate.PairSemantics.raw6958 line 320
  64. def OAI.MUB6.Certificate.PairSemantics.raw6958step0 line 322
  65. def OAI.MUB6.Certificate.PairSemantics.raw6958step1 line 324
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6958 line 326
  67. def OAI.MUB6.Certificate.PairSemantics.raw6959 line 339
  68. def OAI.MUB6.Certificate.PairSemantics.raw6959step0 line 341
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6959 line 343
  70. def OAI.MUB6.Certificate.PairSemantics.raw6960 line 352
  71. def OAI.MUB6.Certificate.PairSemantics.raw6960step0 line 354
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6960 line 356
  73. def OAI.MUB6.Certificate.PairSemantics.raw6961 line 365
  74. def OAI.MUB6.Certificate.PairSemantics.raw6961step0 line 367
  75. def OAI.MUB6.Certificate.PairSemantics.raw6961step1 line 369
  76. def OAI.MUB6.Certificate.PairSemantics.raw6961step2 line 371
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6961 line 373
  78. def OAI.MUB6.Certificate.PairSemantics.raw6962 line 390
  79. def OAI.MUB6.Certificate.PairSemantics.raw6962step0 line 392
  80. def OAI.MUB6.Certificate.PairSemantics.raw6962step1 line 394
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6962 line 396
  82. def OAI.MUB6.Certificate.PairSemantics.raw6963 line 409
  83. def OAI.MUB6.Certificate.PairSemantics.raw6963step0 line 411
  84. def OAI.MUB6.Certificate.PairSemantics.raw6963step1 line 413
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6963 line 415
  86. def OAI.MUB6.Certificate.PairSemantics.raw6964 line 428
  87. def OAI.MUB6.Certificate.PairSemantics.raw6964step0 line 430
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6964 line 432
  89. def OAI.MUB6.Certificate.PairSemantics.raw6965 line 441
  90. def OAI.MUB6.Certificate.PairSemantics.raw6965step0 line 443
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6965 line 445
  92. def OAI.MUB6.Certificate.PairSemantics.raw6966 line 454
  93. def OAI.MUB6.Certificate.PairSemantics.raw6966step0 line 456
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical6966 line 458
  95. def OAI.MUB6.Certificate.PairSemantics.raw6967 line 467
  96. def OAI.MUB6.Certificate.PairSemantics.raw6967step0 line 469
  97. def OAI.MUB6.Certificate.PairSemantics.raw6967step1 line 471
  98. def OAI.MUB6.Certificate.PairSemantics.raw6967step2 line 473
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6967 line 475
  100. def OAI.MUB6.Certificate.PairSemantics.raw6968 line 492
  101. def OAI.MUB6.Certificate.PairSemantics.raw6968step0 line 494
  102. def OAI.MUB6.Certificate.PairSemantics.raw6968step1 line 496
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6968 line 498
  104. def OAI.MUB6.Certificate.PairSemantics.raw6969 line 511
  105. def OAI.MUB6.Certificate.PairSemantics.raw6969step0 line 513
  106. def OAI.MUB6.Certificate.PairSemantics.raw6969step1 line 515
  107. def OAI.MUB6.Certificate.PairSemantics.raw6969step2 line 517
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6969 line 519
  109. def OAI.MUB6.Certificate.PairSemantics.raw6970 line 536
  110. def OAI.MUB6.Certificate.PairSemantics.raw6970step0 line 538
  111. def OAI.MUB6.Certificate.PairSemantics.raw6970step1 line 540
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical6970 line 542
  113. def OAI.MUB6.Certificate.PairSemantics.raw6971 line 555
  114. def OAI.MUB6.Certificate.PairSemantics.raw6971step0 line 557
  115. def OAI.MUB6.Certificate.PairSemantics.raw6971step1 line 559
  116. def OAI.MUB6.Certificate.PairSemantics.raw6971step2 line 561
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical6971 line 563
  118. def OAI.MUB6.Certificate.PairSemantics.raw6972 line 580
  119. def OAI.MUB6.Certificate.PairSemantics.raw6972step0 line 582
  120. def OAI.MUB6.Certificate.PairSemantics.raw6972step1 line 584
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical6972 line 586
  122. def OAI.MUB6.Certificate.PairSemantics.raw6973 line 599
  123. def OAI.MUB6.Certificate.PairSemantics.raw6973step0 line 601
  124. def OAI.MUB6.Certificate.PairSemantics.raw6973step1 line 603
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical6973 line 605
  126. def OAI.MUB6.Certificate.PairSemantics.raw6974 line 618
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical6974 line 620
  128. def OAI.MUB6.Certificate.PairSemantics.raw6975 line 624
  129. def OAI.MUB6.Certificate.PairSemantics.raw6975step0 line 626
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical6975 line 628