OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical276.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8832 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8832step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw8832step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8832 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw8833 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw8833step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw8833step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8833 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw8834 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw8834step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw8834step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8834 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw8835 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw8835step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw8835step1 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8835 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw8836 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw8836step0 line 97
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8836 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw8837 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw8837step0 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw8837step1 line 112
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8837 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw8838 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw8838step0 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw8838step1 line 131
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8838 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw8839 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw8839step0 line 148
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8839 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw8840 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw8840step0 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw8840step1 line 163
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8840 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw8841 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw8841step0 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw8841step1 line 182
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8841 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw8842 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw8842step0 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw8842step1 line 201
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8842 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw8843 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw8843step0 line 218
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8843 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw8844 line 229
  47. def OAI.MUB6.Certificate.PairSemantics.raw8844step0 line 231
  48. def OAI.MUB6.Certificate.PairSemantics.raw8844step1 line 233
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8844 line 235
  50. def OAI.MUB6.Certificate.PairSemantics.raw8845 line 248
  51. def OAI.MUB6.Certificate.PairSemantics.raw8845step0 line 250
  52. def OAI.MUB6.Certificate.PairSemantics.raw8845step1 line 252
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8845 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw8846 line 267
  55. def OAI.MUB6.Certificate.PairSemantics.raw8846step0 line 269
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8846 line 271
  57. def OAI.MUB6.Certificate.PairSemantics.raw8847 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw8847step0 line 282
  59. def OAI.MUB6.Certificate.PairSemantics.raw8847step1 line 284
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8847 line 286
  61. def OAI.MUB6.Certificate.PairSemantics.raw8848 line 299
  62. def OAI.MUB6.Certificate.PairSemantics.raw8848step0 line 301
  63. def OAI.MUB6.Certificate.PairSemantics.raw8848step1 line 303
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8848 line 305
  65. def OAI.MUB6.Certificate.PairSemantics.raw8849 line 318
  66. def OAI.MUB6.Certificate.PairSemantics.raw8849step0 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw8849step1 line 322
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8849 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw8850 line 337
  70. def OAI.MUB6.Certificate.PairSemantics.raw8850step0 line 339
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8850 line 341
  72. def OAI.MUB6.Certificate.PairSemantics.raw8851 line 350
  73. def OAI.MUB6.Certificate.PairSemantics.raw8851step0 line 352
  74. def OAI.MUB6.Certificate.PairSemantics.raw8851step1 line 354
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8851 line 356
  76. def OAI.MUB6.Certificate.PairSemantics.raw8852 line 369
  77. def OAI.MUB6.Certificate.PairSemantics.raw8852step0 line 371
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical8852 line 373
  79. def OAI.MUB6.Certificate.PairSemantics.raw8853 line 382
  80. def OAI.MUB6.Certificate.PairSemantics.raw8853step0 line 384
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8853 line 386
  82. def OAI.MUB6.Certificate.PairSemantics.raw8854 line 395
  83. def OAI.MUB6.Certificate.PairSemantics.raw8854step0 line 397
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical8854 line 399
  85. def OAI.MUB6.Certificate.PairSemantics.raw8855 line 408
  86. def OAI.MUB6.Certificate.PairSemantics.raw8855step0 line 410
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical8855 line 412
  88. def OAI.MUB6.Certificate.PairSemantics.raw8856 line 421
  89. def OAI.MUB6.Certificate.PairSemantics.raw8856step0 line 423
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical8856 line 425
  91. def OAI.MUB6.Certificate.PairSemantics.raw8857 line 434
  92. def OAI.MUB6.Certificate.PairSemantics.raw8857step0 line 436
  93. def OAI.MUB6.Certificate.PairSemantics.raw8857step1 line 438
  94. def OAI.MUB6.Certificate.PairSemantics.raw8857step2 line 440
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical8857 line 442
  96. def OAI.MUB6.Certificate.PairSemantics.raw8858 line 460
  97. def OAI.MUB6.Certificate.PairSemantics.raw8858step0 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw8858step1 line 464
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8858 line 466
  100. def OAI.MUB6.Certificate.PairSemantics.raw8859 line 479
  101. def OAI.MUB6.Certificate.PairSemantics.raw8859step0 line 481
  102. def OAI.MUB6.Certificate.PairSemantics.raw8859step1 line 483
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical8859 line 485
  104. def OAI.MUB6.Certificate.PairSemantics.raw8860 line 498
  105. def OAI.MUB6.Certificate.PairSemantics.raw8860step0 line 500
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8860 line 502
  107. def OAI.MUB6.Certificate.PairSemantics.raw8861 line 511
  108. def OAI.MUB6.Certificate.PairSemantics.raw8861step0 line 513
  109. def OAI.MUB6.Certificate.PairSemantics.raw8861step1 line 515
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8861 line 517
  111. def OAI.MUB6.Certificate.PairSemantics.raw8862 line 530
  112. def OAI.MUB6.Certificate.PairSemantics.raw8862step0 line 532
  113. def OAI.MUB6.Certificate.PairSemantics.raw8862step1 line 534
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8862 line 536
  115. def OAI.MUB6.Certificate.PairSemantics.raw8863 line 549
  116. def OAI.MUB6.Certificate.PairSemantics.raw8863step0 line 551
  117. def OAI.MUB6.Certificate.PairSemantics.raw8863step1 line 553
  118. def OAI.MUB6.Certificate.PairSemantics.raw8863step2 line 555
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical8863 line 557