OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical119.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3808 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw3808step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw3808step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3808 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw3809 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw3809step0 line 37
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3809 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw3810 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw3810step0 line 50
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical3810 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw3811 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw3811step0 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw3811step1 line 65
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3811 line 67
  15. def OAI.MUB6.Certificate.PairSemantics.raw3812 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw3812step0 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw3812step1 line 85
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3812 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw3813 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw3813step0 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3813 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw3814 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw3814step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw3814step1 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3814 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw3815 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw3815step0 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw3815step1 line 136
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3815 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw3816 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw3816step0 line 153
  32. def OAI.MUB6.Certificate.PairSemantics.raw3816step1 line 155
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3816 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw3817 line 170
  35. def OAI.MUB6.Certificate.PairSemantics.raw3817step0 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw3817step1 line 174
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3817 line 176
  38. def OAI.MUB6.Certificate.PairSemantics.raw3818 line 189
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3818 line 191
  40. def OAI.MUB6.Certificate.PairSemantics.raw3819 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw3819step0 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw3819step1 line 199
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3819 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw3820 line 214
  45. def OAI.MUB6.Certificate.PairSemantics.raw3820step0 line 216
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3820 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw3821 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw3821step0 line 229
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3821 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw3822 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw3822step0 line 242
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3822 line 244
  53. def OAI.MUB6.Certificate.PairSemantics.raw3823 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw3823step0 line 255
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3823 line 257
  56. def OAI.MUB6.Certificate.PairSemantics.raw3824 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw3824step0 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw3824step1 line 270
  59. def OAI.MUB6.Certificate.PairSemantics.raw3824step2 line 272
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical3824 line 274
  61. def OAI.MUB6.Certificate.PairSemantics.raw3825 line 291
  62. def OAI.MUB6.Certificate.PairSemantics.raw3825step0 line 293
  63. def OAI.MUB6.Certificate.PairSemantics.raw3825step1 line 295
  64. def OAI.MUB6.Certificate.PairSemantics.raw3825step2 line 297
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3825 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw3826 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw3826step0 line 318
  68. def OAI.MUB6.Certificate.PairSemantics.raw3826step1 line 320
  69. def OAI.MUB6.Certificate.PairSemantics.raw3826step2 line 322
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3826 line 324
  71. def OAI.MUB6.Certificate.PairSemantics.raw3827 line 341
  72. def OAI.MUB6.Certificate.PairSemantics.raw3827step0 line 343
  73. def OAI.MUB6.Certificate.PairSemantics.raw3827step1 line 345
  74. def OAI.MUB6.Certificate.PairSemantics.raw3827step2 line 347
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3827 line 349
  76. def OAI.MUB6.Certificate.PairSemantics.raw3828 line 366
  77. def OAI.MUB6.Certificate.PairSemantics.raw3828step0 line 368
  78. def OAI.MUB6.Certificate.PairSemantics.raw3828step1 line 370
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3828 line 372
  80. def OAI.MUB6.Certificate.PairSemantics.raw3829 line 385
  81. def OAI.MUB6.Certificate.PairSemantics.raw3829step0 line 387
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3829 line 389
  83. def OAI.MUB6.Certificate.PairSemantics.raw3830 line 398
  84. def OAI.MUB6.Certificate.PairSemantics.raw3830step0 line 400
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3830 line 402
  86. def OAI.MUB6.Certificate.PairSemantics.raw3831 line 411
  87. def OAI.MUB6.Certificate.PairSemantics.raw3831step0 line 413
  88. def OAI.MUB6.Certificate.PairSemantics.raw3831step1 line 415
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3831 line 417
  90. def OAI.MUB6.Certificate.PairSemantics.raw3832 line 430
  91. def OAI.MUB6.Certificate.PairSemantics.raw3832step0 line 432
  92. def OAI.MUB6.Certificate.PairSemantics.raw3832step1 line 434
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3832 line 436
  94. def OAI.MUB6.Certificate.PairSemantics.raw3833 line 449
  95. def OAI.MUB6.Certificate.PairSemantics.raw3833step0 line 451
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3833 line 453
  97. def OAI.MUB6.Certificate.PairSemantics.raw3834 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw3834step0 line 464
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3834 line 466
  100. def OAI.MUB6.Certificate.PairSemantics.raw3835 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw3835step0 line 477
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3835 line 479
  103. def OAI.MUB6.Certificate.PairSemantics.raw3836 line 488
  104. def OAI.MUB6.Certificate.PairSemantics.raw3836step0 line 490
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3836 line 492
  106. def OAI.MUB6.Certificate.PairSemantics.raw3837 line 501
  107. def OAI.MUB6.Certificate.PairSemantics.raw3837step0 line 503
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical3837 line 505
  109. def OAI.MUB6.Certificate.PairSemantics.raw3838 line 514
  110. def OAI.MUB6.Certificate.PairSemantics.raw3838step0 line 516
  111. def OAI.MUB6.Certificate.PairSemantics.raw3838step1 line 518
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical3838 line 520
  113. def OAI.MUB6.Certificate.PairSemantics.raw3839 line 533
  114. def OAI.MUB6.Certificate.PairSemantics.raw3839step0 line 535
  115. def OAI.MUB6.Certificate.PairSemantics.raw3839step1 line 537
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical3839 line 539