OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical215.lean

GitHub source file

150 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6880 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw6880step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6880 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw6881 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw6881step0 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6881 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw6882 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw6882step0 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw6882step1 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6882 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw6883 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw6883step0 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw6883step1 line 65
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6883 line 67
  15. def OAI.MUB6.Certificate.PairSemantics.raw6884 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw6884step0 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6884 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw6885 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw6885step0 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw6885step1 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6885 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw6886 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw6886step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw6886step1 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6886 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw6887 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw6887step0 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw6887step1 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw6887step2 line 138
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6887 line 140
  31. def OAI.MUB6.Certificate.PairSemantics.raw6888 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw6888step0 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw6888step1 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw6888step2 line 163
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6888 line 165
  36. def OAI.MUB6.Certificate.PairSemantics.raw6889 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw6889step0 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw6889step1 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw6889step2 line 188
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6889 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw6890 line 207
  42. def OAI.MUB6.Certificate.PairSemantics.raw6890step0 line 209
  43. def OAI.MUB6.Certificate.PairSemantics.raw6890step1 line 211
  44. def OAI.MUB6.Certificate.PairSemantics.raw6890step2 line 213
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6890 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw6891 line 232
  47. def OAI.MUB6.Certificate.PairSemantics.raw6891step0 line 234
  48. def OAI.MUB6.Certificate.PairSemantics.raw6891step1 line 236
  49. def OAI.MUB6.Certificate.PairSemantics.raw6891step2 line 238
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6891 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw6892 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw6892step0 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw6892step1 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw6892step2 line 263
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6892 line 265
  56. def OAI.MUB6.Certificate.PairSemantics.raw6893 line 282
  57. def OAI.MUB6.Certificate.PairSemantics.raw6893step0 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw6893step1 line 286
  59. def OAI.MUB6.Certificate.PairSemantics.raw6893step2 line 288
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6893 line 290
  61. def OAI.MUB6.Certificate.PairSemantics.raw6894 line 307
  62. def OAI.MUB6.Certificate.PairSemantics.raw6894step0 line 309
  63. def OAI.MUB6.Certificate.PairSemantics.raw6894step1 line 311
  64. def OAI.MUB6.Certificate.PairSemantics.raw6894step2 line 313
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6894 line 315
  66. def OAI.MUB6.Certificate.PairSemantics.raw6895 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw6895step0 line 334
  68. def OAI.MUB6.Certificate.PairSemantics.raw6895step1 line 336
  69. def OAI.MUB6.Certificate.PairSemantics.raw6895step2 line 338
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6895 line 340
  71. def OAI.MUB6.Certificate.PairSemantics.raw6896 line 357
  72. def OAI.MUB6.Certificate.PairSemantics.raw6896step0 line 359
  73. def OAI.MUB6.Certificate.PairSemantics.raw6896step1 line 361
  74. def OAI.MUB6.Certificate.PairSemantics.raw6896step2 line 363
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6896 line 365
  76. def OAI.MUB6.Certificate.PairSemantics.raw6897 line 382
  77. def OAI.MUB6.Certificate.PairSemantics.raw6897step0 line 384
  78. def OAI.MUB6.Certificate.PairSemantics.raw6897step1 line 386
  79. def OAI.MUB6.Certificate.PairSemantics.raw6897step2 line 388
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6897 line 390
  81. def OAI.MUB6.Certificate.PairSemantics.raw6898 line 407
  82. def OAI.MUB6.Certificate.PairSemantics.raw6898step0 line 409
  83. def OAI.MUB6.Certificate.PairSemantics.raw6898step1 line 411
  84. def OAI.MUB6.Certificate.PairSemantics.raw6898step2 line 413
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6898 line 415
  86. def OAI.MUB6.Certificate.PairSemantics.raw6899 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw6899step0 line 434
  88. def OAI.MUB6.Certificate.PairSemantics.raw6899step1 line 436
  89. def OAI.MUB6.Certificate.PairSemantics.raw6899step2 line 438
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6899 line 440
  91. def OAI.MUB6.Certificate.PairSemantics.raw6900 line 457
  92. def OAI.MUB6.Certificate.PairSemantics.raw6900step0 line 459
  93. def OAI.MUB6.Certificate.PairSemantics.raw6900step1 line 461
  94. def OAI.MUB6.Certificate.PairSemantics.raw6900step2 line 463
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6900 line 465
  96. def OAI.MUB6.Certificate.PairSemantics.raw6901 line 482
  97. def OAI.MUB6.Certificate.PairSemantics.raw6901step0 line 484
  98. def OAI.MUB6.Certificate.PairSemantics.raw6901step1 line 486
  99. def OAI.MUB6.Certificate.PairSemantics.raw6901step2 line 488
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical6901 line 490
  101. def OAI.MUB6.Certificate.PairSemantics.raw6902 line 507
  102. def OAI.MUB6.Certificate.PairSemantics.raw6902step0 line 509
  103. def OAI.MUB6.Certificate.PairSemantics.raw6902step1 line 511
  104. def OAI.MUB6.Certificate.PairSemantics.raw6902step2 line 513
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical6902 line 515
  106. def OAI.MUB6.Certificate.PairSemantics.raw6903 line 532
  107. def OAI.MUB6.Certificate.PairSemantics.raw6903step0 line 534
  108. def OAI.MUB6.Certificate.PairSemantics.raw6903step1 line 536
  109. def OAI.MUB6.Certificate.PairSemantics.raw6903step2 line 538
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical6903 line 540
  111. def OAI.MUB6.Certificate.PairSemantics.raw6904 line 557
  112. def OAI.MUB6.Certificate.PairSemantics.raw6904step0 line 559
  113. def OAI.MUB6.Certificate.PairSemantics.raw6904step1 line 561
  114. def OAI.MUB6.Certificate.PairSemantics.raw6904step2 line 563
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical6904 line 565
  116. def OAI.MUB6.Certificate.PairSemantics.raw6905 line 582
  117. def OAI.MUB6.Certificate.PairSemantics.raw6905step0 line 584
  118. def OAI.MUB6.Certificate.PairSemantics.raw6905step1 line 586
  119. def OAI.MUB6.Certificate.PairSemantics.raw6905step2 line 588
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical6905 line 590
  121. def OAI.MUB6.Certificate.PairSemantics.raw6906 line 607
  122. def OAI.MUB6.Certificate.PairSemantics.raw6906step0 line 609
  123. def OAI.MUB6.Certificate.PairSemantics.raw6906step1 line 611
  124. def OAI.MUB6.Certificate.PairSemantics.raw6906step2 line 613
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical6906 line 615
  126. def OAI.MUB6.Certificate.PairSemantics.raw6907 line 632
  127. def OAI.MUB6.Certificate.PairSemantics.raw6907step0 line 634
  128. def OAI.MUB6.Certificate.PairSemantics.raw6907step1 line 636
  129. def OAI.MUB6.Certificate.PairSemantics.raw6907step2 line 638
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical6907 line 640
  131. def OAI.MUB6.Certificate.PairSemantics.raw6908 line 657
  132. def OAI.MUB6.Certificate.PairSemantics.raw6908step0 line 659
  133. def OAI.MUB6.Certificate.PairSemantics.raw6908step1 line 661
  134. def OAI.MUB6.Certificate.PairSemantics.raw6908step2 line 663
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical6908 line 665
  136. def OAI.MUB6.Certificate.PairSemantics.raw6909 line 682
  137. def OAI.MUB6.Certificate.PairSemantics.raw6909step0 line 684
  138. def OAI.MUB6.Certificate.PairSemantics.raw6909step1 line 686
  139. def OAI.MUB6.Certificate.PairSemantics.raw6909step2 line 688
  140. theorem OAI.MUB6.Certificate.PairSemantics.canonical6909 line 690
  141. def OAI.MUB6.Certificate.PairSemantics.raw6910 line 707
  142. def OAI.MUB6.Certificate.PairSemantics.raw6910step0 line 709
  143. def OAI.MUB6.Certificate.PairSemantics.raw6910step1 line 711
  144. def OAI.MUB6.Certificate.PairSemantics.raw6910step2 line 713
  145. theorem OAI.MUB6.Certificate.PairSemantics.canonical6910 line 715
  146. def OAI.MUB6.Certificate.PairSemantics.raw6911 line 732
  147. def OAI.MUB6.Certificate.PairSemantics.raw6911step0 line 734
  148. def OAI.MUB6.Certificate.PairSemantics.raw6911step1 line 736
  149. def OAI.MUB6.Certificate.PairSemantics.raw6911step2 line 738
  150. theorem OAI.MUB6.Certificate.PairSemantics.canonical6911 line 740