OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical27.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw864 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw864step0 line 12
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical864 line 14
  4. def OAI.MUB6.Certificate.PairSemantics.raw865 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw865step0 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical865 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw866 line 38
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical866 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw867 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical867 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw868 line 50
  12. def OAI.MUB6.Certificate.PairSemantics.raw868step0 line 52
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical868 line 54
  14. def OAI.MUB6.Certificate.PairSemantics.raw869 line 63
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical869 line 65
  16. def OAI.MUB6.Certificate.PairSemantics.raw870 line 69
  17. def OAI.MUB6.Certificate.PairSemantics.raw870step0 line 71
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical870 line 73
  19. def OAI.MUB6.Certificate.PairSemantics.raw871 line 83
  20. def OAI.MUB6.Certificate.PairSemantics.raw871step0 line 85
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical871 line 87
  22. def OAI.MUB6.Certificate.PairSemantics.raw872 line 96
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical872 line 98
  24. def OAI.MUB6.Certificate.PairSemantics.raw873 line 102
  25. def OAI.MUB6.Certificate.PairSemantics.raw873step0 line 104
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical873 line 106
  27. def OAI.MUB6.Certificate.PairSemantics.raw874 line 115
  28. def OAI.MUB6.Certificate.PairSemantics.raw874step0 line 117
  29. def OAI.MUB6.Certificate.PairSemantics.raw874step1 line 119
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical874 line 121
  31. def OAI.MUB6.Certificate.PairSemantics.raw875 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw875step0 line 138
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical875 line 140
  34. def OAI.MUB6.Certificate.PairSemantics.raw876 line 150
  35. def OAI.MUB6.Certificate.PairSemantics.raw876step0 line 152
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical876 line 154
  37. def OAI.MUB6.Certificate.PairSemantics.raw877 line 164
  38. def OAI.MUB6.Certificate.PairSemantics.raw877step0 line 166
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical877 line 168
  40. def OAI.MUB6.Certificate.PairSemantics.raw878 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw878step0 line 180
  42. def OAI.MUB6.Certificate.PairSemantics.raw878step1 line 182
  43. def OAI.MUB6.Certificate.PairSemantics.raw878step2 line 184
  44. def OAI.MUB6.Certificate.PairSemantics.raw878step3 line 186
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical878 line 188
  46. def OAI.MUB6.Certificate.PairSemantics.raw879 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw879step0 line 215
  48. def OAI.MUB6.Certificate.PairSemantics.raw879step1 line 217
  49. def OAI.MUB6.Certificate.PairSemantics.raw879step2 line 219
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical879 line 221
  51. def OAI.MUB6.Certificate.PairSemantics.raw880 line 241
  52. def OAI.MUB6.Certificate.PairSemantics.raw880step0 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw880step1 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw880step2 line 247
  55. def OAI.MUB6.Certificate.PairSemantics.raw880step3 line 249
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical880 line 251
  57. def OAI.MUB6.Certificate.PairSemantics.raw881 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw881step0 line 277
  59. def OAI.MUB6.Certificate.PairSemantics.raw881step1 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw881step2 line 281
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical881 line 283
  62. def OAI.MUB6.Certificate.PairSemantics.raw882 line 303
  63. def OAI.MUB6.Certificate.PairSemantics.raw882step0 line 305
  64. def OAI.MUB6.Certificate.PairSemantics.raw882step1 line 307
  65. def OAI.MUB6.Certificate.PairSemantics.raw882step2 line 309
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical882 line 311
  67. def OAI.MUB6.Certificate.PairSemantics.raw883 line 331
  68. def OAI.MUB6.Certificate.PairSemantics.raw883step0 line 333
  69. def OAI.MUB6.Certificate.PairSemantics.raw883step1 line 335
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical883 line 337
  71. def OAI.MUB6.Certificate.PairSemantics.raw884 line 352
  72. def OAI.MUB6.Certificate.PairSemantics.raw884step0 line 354
  73. def OAI.MUB6.Certificate.PairSemantics.raw884step1 line 356
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical884 line 358
  75. def OAI.MUB6.Certificate.PairSemantics.raw885 line 373
  76. def OAI.MUB6.Certificate.PairSemantics.raw885step0 line 375
  77. def OAI.MUB6.Certificate.PairSemantics.raw885step1 line 377
  78. def OAI.MUB6.Certificate.PairSemantics.raw885step2 line 379
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical885 line 381
  80. def OAI.MUB6.Certificate.PairSemantics.raw886 line 401
  81. def OAI.MUB6.Certificate.PairSemantics.raw886step0 line 403
  82. def OAI.MUB6.Certificate.PairSemantics.raw886step1 line 405
  83. def OAI.MUB6.Certificate.PairSemantics.raw886step2 line 407
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical886 line 409
  85. def OAI.MUB6.Certificate.PairSemantics.raw887 line 428
  86. def OAI.MUB6.Certificate.PairSemantics.raw887step0 line 430
  87. def OAI.MUB6.Certificate.PairSemantics.raw887step1 line 432
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical887 line 434
  89. def OAI.MUB6.Certificate.PairSemantics.raw888 line 449
  90. def OAI.MUB6.Certificate.PairSemantics.raw888step0 line 451
  91. def OAI.MUB6.Certificate.PairSemantics.raw888step1 line 453
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical888 line 455
  93. def OAI.MUB6.Certificate.PairSemantics.raw889 line 469
  94. def OAI.MUB6.Certificate.PairSemantics.raw889step0 line 471
  95. def OAI.MUB6.Certificate.PairSemantics.raw889step1 line 473
  96. def OAI.MUB6.Certificate.PairSemantics.raw889step2 line 475
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical889 line 477
  98. def OAI.MUB6.Certificate.PairSemantics.raw890 line 497
  99. def OAI.MUB6.Certificate.PairSemantics.raw890step0 line 499
  100. def OAI.MUB6.Certificate.PairSemantics.raw890step1 line 501
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical890 line 503
  102. def OAI.MUB6.Certificate.PairSemantics.raw891 line 518
  103. def OAI.MUB6.Certificate.PairSemantics.raw891step0 line 520
  104. def OAI.MUB6.Certificate.PairSemantics.raw891step1 line 522
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical891 line 524
  106. def OAI.MUB6.Certificate.PairSemantics.raw892 line 539
  107. def OAI.MUB6.Certificate.PairSemantics.raw892step0 line 541
  108. def OAI.MUB6.Certificate.PairSemantics.raw892step1 line 543
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical892 line 545
  110. def OAI.MUB6.Certificate.PairSemantics.raw893 line 560
  111. def OAI.MUB6.Certificate.PairSemantics.raw893step0 line 562
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical893 line 564
  113. def OAI.MUB6.Certificate.PairSemantics.raw894 line 574
  114. def OAI.MUB6.Certificate.PairSemantics.raw894step0 line 576
  115. def OAI.MUB6.Certificate.PairSemantics.raw894step1 line 578
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical894 line 580
  117. def OAI.MUB6.Certificate.PairSemantics.raw895 line 595
  118. def OAI.MUB6.Certificate.PairSemantics.raw895step0 line 597
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical895 line 599