OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical116.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3712 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw3712step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw3712step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3712 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw3713 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw3713step0 line 42
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3713 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw3714 line 53
  9. def OAI.MUB6.Certificate.PairSemantics.raw3714step0 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw3714step1 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3714 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw3715 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw3715step0 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw3715step1 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3715 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw3716 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw3716step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw3716step1 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3716 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw3717 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw3717step0 line 112
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3717 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw3718 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw3718step0 line 125
  25. def OAI.MUB6.Certificate.PairSemantics.raw3718step1 line 127
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3718 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw3719 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw3719step0 line 144
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3719 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw3720 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw3720step0 line 157
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3720 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw3721 line 168
  34. def OAI.MUB6.Certificate.PairSemantics.raw3721step0 line 170
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3721 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw3722 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw3722step0 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw3722step1 line 185
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3722 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw3723 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw3723step0 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw3723step1 line 204
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3723 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw3724 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw3724step0 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw3724step1 line 223
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3724 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw3725 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw3725step0 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw3725step1 line 242
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3725 line 244
  52. def OAI.MUB6.Certificate.PairSemantics.raw3726 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3726 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw3727 line 263
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3727 line 265
  56. def OAI.MUB6.Certificate.PairSemantics.raw3728 line 269
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3728 line 271
  58. def OAI.MUB6.Certificate.PairSemantics.raw3729 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw3729step0 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw3729step1 line 279
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3729 line 281
  62. def OAI.MUB6.Certificate.PairSemantics.raw3730 line 294
  63. def OAI.MUB6.Certificate.PairSemantics.raw3730step0 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw3730step1 line 298
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3730 line 300
  66. def OAI.MUB6.Certificate.PairSemantics.raw3731 line 313
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical3731 line 315
  68. def OAI.MUB6.Certificate.PairSemantics.raw3732 line 319
  69. def OAI.MUB6.Certificate.PairSemantics.raw3732step0 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw3732step1 line 323
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical3732 line 325
  72. def OAI.MUB6.Certificate.PairSemantics.raw3733 line 338
  73. def OAI.MUB6.Certificate.PairSemantics.raw3733step0 line 340
  74. def OAI.MUB6.Certificate.PairSemantics.raw3733step1 line 342
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3733 line 344
  76. def OAI.MUB6.Certificate.PairSemantics.raw3734 line 357
  77. def OAI.MUB6.Certificate.PairSemantics.raw3734step0 line 359
  78. def OAI.MUB6.Certificate.PairSemantics.raw3734step1 line 361
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3734 line 363
  80. def OAI.MUB6.Certificate.PairSemantics.raw3735 line 376
  81. def OAI.MUB6.Certificate.PairSemantics.raw3735step0 line 378
  82. def OAI.MUB6.Certificate.PairSemantics.raw3735step1 line 380
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3735 line 382
  84. def OAI.MUB6.Certificate.PairSemantics.raw3736 line 395
  85. def OAI.MUB6.Certificate.PairSemantics.raw3736step0 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw3736step1 line 399
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3736 line 401
  88. def OAI.MUB6.Certificate.PairSemantics.raw3737 line 414
  89. def OAI.MUB6.Certificate.PairSemantics.raw3737step0 line 416
  90. def OAI.MUB6.Certificate.PairSemantics.raw3737step1 line 418
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3737 line 420
  92. def OAI.MUB6.Certificate.PairSemantics.raw3738 line 433
  93. def OAI.MUB6.Certificate.PairSemantics.raw3738step0 line 435
  94. def OAI.MUB6.Certificate.PairSemantics.raw3738step1 line 437
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical3738 line 439
  96. def OAI.MUB6.Certificate.PairSemantics.raw3739 line 452
  97. def OAI.MUB6.Certificate.PairSemantics.raw3739step0 line 454
  98. def OAI.MUB6.Certificate.PairSemantics.raw3739step1 line 456
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3739 line 458
  100. def OAI.MUB6.Certificate.PairSemantics.raw3740 line 471
  101. def OAI.MUB6.Certificate.PairSemantics.raw3740step0 line 473
  102. def OAI.MUB6.Certificate.PairSemantics.raw3740step1 line 475
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3740 line 477
  104. def OAI.MUB6.Certificate.PairSemantics.raw3741 line 490
  105. def OAI.MUB6.Certificate.PairSemantics.raw3741step0 line 492
  106. def OAI.MUB6.Certificate.PairSemantics.raw3741step1 line 494
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3741 line 496
  108. def OAI.MUB6.Certificate.PairSemantics.raw3742 line 509
  109. def OAI.MUB6.Certificate.PairSemantics.raw3742step0 line 511
  110. def OAI.MUB6.Certificate.PairSemantics.raw3742step1 line 513
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical3742 line 515
  112. def OAI.MUB6.Certificate.PairSemantics.raw3743 line 528
  113. def OAI.MUB6.Certificate.PairSemantics.raw3743step0 line 530
  114. def OAI.MUB6.Certificate.PairSemantics.raw3743step1 line 532
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical3743 line 534