OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical118.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3776 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw3776step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw3776step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3776 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw3777 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw3777step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw3777step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3777 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw3778 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw3778step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw3778step1 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3778 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw3779 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw3779step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw3779step1 line 81
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3779 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw3780 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw3780step0 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw3780step1 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3780 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw3781 line 115
  22. def OAI.MUB6.Certificate.PairSemantics.raw3781step0 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw3781step1 line 119
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3781 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw3782 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw3782step0 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw3782step1 line 138
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3782 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw3783 line 153
  30. def OAI.MUB6.Certificate.PairSemantics.raw3783step0 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw3783step1 line 157
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3783 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw3784 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw3784step0 line 174
  35. def OAI.MUB6.Certificate.PairSemantics.raw3784step1 line 176
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3784 line 178
  37. def OAI.MUB6.Certificate.PairSemantics.raw3785 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw3785step0 line 193
  39. def OAI.MUB6.Certificate.PairSemantics.raw3785step1 line 195
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3785 line 197
  41. def OAI.MUB6.Certificate.PairSemantics.raw3786 line 210
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3786 line 212
  43. def OAI.MUB6.Certificate.PairSemantics.raw3787 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw3787step0 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw3787step1 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw3787step2 line 222
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3787 line 224
  48. def OAI.MUB6.Certificate.PairSemantics.raw3788 line 241
  49. def OAI.MUB6.Certificate.PairSemantics.raw3788step0 line 243
  50. def OAI.MUB6.Certificate.PairSemantics.raw3788step1 line 245
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3788 line 247
  52. def OAI.MUB6.Certificate.PairSemantics.raw3789 line 260
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3789 line 262
  54. def OAI.MUB6.Certificate.PairSemantics.raw3790 line 266
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3790 line 268
  56. def OAI.MUB6.Certificate.PairSemantics.raw3791 line 272
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3791 line 274
  58. def OAI.MUB6.Certificate.PairSemantics.raw3792 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw3792step0 line 280
  60. def OAI.MUB6.Certificate.PairSemantics.raw3792step1 line 282
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3792 line 284
  62. def OAI.MUB6.Certificate.PairSemantics.raw3793 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw3793step0 line 299
  64. def OAI.MUB6.Certificate.PairSemantics.raw3793step1 line 301
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3793 line 303
  66. def OAI.MUB6.Certificate.PairSemantics.raw3794 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw3794step0 line 318
  68. def OAI.MUB6.Certificate.PairSemantics.raw3794step1 line 320
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3794 line 322
  70. def OAI.MUB6.Certificate.PairSemantics.raw3795 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw3795step0 line 337
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3795 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw3796 line 348
  74. def OAI.MUB6.Certificate.PairSemantics.raw3796step0 line 350
  75. def OAI.MUB6.Certificate.PairSemantics.raw3796step1 line 352
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3796 line 354
  77. def OAI.MUB6.Certificate.PairSemantics.raw3797 line 367
  78. def OAI.MUB6.Certificate.PairSemantics.raw3797step0 line 369
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3797 line 371
  80. def OAI.MUB6.Certificate.PairSemantics.raw3798 line 380
  81. def OAI.MUB6.Certificate.PairSemantics.raw3798step0 line 382
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3798 line 384
  83. def OAI.MUB6.Certificate.PairSemantics.raw3799 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw3799step0 line 395
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3799 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw3800 line 406
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3800 line 408
  88. def OAI.MUB6.Certificate.PairSemantics.raw3801 line 412
  89. def OAI.MUB6.Certificate.PairSemantics.raw3801step0 line 414
  90. def OAI.MUB6.Certificate.PairSemantics.raw3801step1 line 416
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3801 line 418
  92. def OAI.MUB6.Certificate.PairSemantics.raw3802 line 431
  93. def OAI.MUB6.Certificate.PairSemantics.raw3802step0 line 433
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3802 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw3803 line 444
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3803 line 446
  97. def OAI.MUB6.Certificate.PairSemantics.raw3804 line 450
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3804 line 452
  99. def OAI.MUB6.Certificate.PairSemantics.raw3805 line 456
  100. def OAI.MUB6.Certificate.PairSemantics.raw3805step0 line 458
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3805 line 460
  102. def OAI.MUB6.Certificate.PairSemantics.raw3806 line 469
  103. def OAI.MUB6.Certificate.PairSemantics.raw3806step0 line 471
  104. def OAI.MUB6.Certificate.PairSemantics.raw3806step1 line 473
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3806 line 475
  106. def OAI.MUB6.Certificate.PairSemantics.raw3807 line 488
  107. def OAI.MUB6.Certificate.PairSemantics.raw3807step0 line 490
  108. def OAI.MUB6.Certificate.PairSemantics.raw3807step1 line 492
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3807 line 494