OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical236.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7552 line 21
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical7552 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw7553 line 27
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7553 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw7554 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw7554step0 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw7554step1 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7554 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw7555 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw7555step0 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw7555step1 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw7555step2 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7555 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw7556 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw7556step0 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw7556step1 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw7556step2 line 83
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical7556 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw7557 line 102
  20. def OAI.MUB6.Certificate.PairSemantics.raw7557step0 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw7557step1 line 106
  22. def OAI.MUB6.Certificate.PairSemantics.raw7557step2 line 108
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7557 line 110
  24. def OAI.MUB6.Certificate.PairSemantics.raw7558 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw7558step0 line 129
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7558 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw7559 line 140
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7559 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw7560 line 146
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7560 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw7561 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw7561step0 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw7561step1 line 156
  34. def OAI.MUB6.Certificate.PairSemantics.raw7561step2 line 158
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7561 line 160
  36. def OAI.MUB6.Certificate.PairSemantics.raw7562 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw7562step0 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw7562step1 line 181
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7562 line 183
  40. def OAI.MUB6.Certificate.PairSemantics.raw7563 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw7563step0 line 198
  42. def OAI.MUB6.Certificate.PairSemantics.raw7563step1 line 200
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7563 line 202
  44. def OAI.MUB6.Certificate.PairSemantics.raw7564 line 215
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7564 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw7565 line 221
  47. def OAI.MUB6.Certificate.PairSemantics.raw7565step0 line 223
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7565 line 225
  49. def OAI.MUB6.Certificate.PairSemantics.raw7566 line 234
  50. def OAI.MUB6.Certificate.PairSemantics.raw7566step0 line 236
  51. def OAI.MUB6.Certificate.PairSemantics.raw7566step1 line 238
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7566 line 240
  53. def OAI.MUB6.Certificate.PairSemantics.raw7567 line 253
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7567 line 255
  55. def OAI.MUB6.Certificate.PairSemantics.raw7568 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw7568step0 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw7568step1 line 263
  58. def OAI.MUB6.Certificate.PairSemantics.raw7568step2 line 265
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7568 line 267
  60. def OAI.MUB6.Certificate.PairSemantics.raw7569 line 284
  61. def OAI.MUB6.Certificate.PairSemantics.raw7569step0 line 286
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7569 line 288
  63. def OAI.MUB6.Certificate.PairSemantics.raw7570 line 297
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical7570 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw7571 line 303
  66. def OAI.MUB6.Certificate.PairSemantics.raw7571step0 line 305
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical7571 line 307
  68. def OAI.MUB6.Certificate.PairSemantics.raw7572 line 316
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7572 line 318
  70. def OAI.MUB6.Certificate.PairSemantics.raw7573 line 322
  71. def OAI.MUB6.Certificate.PairSemantics.raw7573step0 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw7573step1 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw7573step2 line 328
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7573 line 330
  75. def OAI.MUB6.Certificate.PairSemantics.raw7574 line 348
  76. def OAI.MUB6.Certificate.PairSemantics.raw7574step0 line 350
  77. def OAI.MUB6.Certificate.PairSemantics.raw7574step1 line 352
  78. def OAI.MUB6.Certificate.PairSemantics.raw7574step2 line 354
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical7574 line 356
  80. def OAI.MUB6.Certificate.PairSemantics.raw7575 line 374
  81. def OAI.MUB6.Certificate.PairSemantics.raw7575step0 line 376
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7575 line 378
  83. def OAI.MUB6.Certificate.PairSemantics.raw7576 line 387
  84. def OAI.MUB6.Certificate.PairSemantics.raw7576step0 line 389
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7576 line 391
  86. def OAI.MUB6.Certificate.PairSemantics.raw7577 line 400
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7577 line 402
  88. def OAI.MUB6.Certificate.PairSemantics.raw7578 line 406
  89. def OAI.MUB6.Certificate.PairSemantics.raw7578step0 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw7578step1 line 410
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7578 line 412
  92. def OAI.MUB6.Certificate.PairSemantics.raw7579 line 425
  93. def OAI.MUB6.Certificate.PairSemantics.raw7579step0 line 427
  94. def OAI.MUB6.Certificate.PairSemantics.raw7579step1 line 429
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7579 line 431
  96. def OAI.MUB6.Certificate.PairSemantics.raw7580 line 444
  97. def OAI.MUB6.Certificate.PairSemantics.raw7580step0 line 446
  98. def OAI.MUB6.Certificate.PairSemantics.raw7580step1 line 448
  99. def OAI.MUB6.Certificate.PairSemantics.raw7580step2 line 450
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical7580 line 452
  101. def OAI.MUB6.Certificate.PairSemantics.raw7581 line 469
  102. def OAI.MUB6.Certificate.PairSemantics.raw7581step0 line 471
  103. def OAI.MUB6.Certificate.PairSemantics.raw7581step1 line 473
  104. def OAI.MUB6.Certificate.PairSemantics.raw7581step2 line 475
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7581 line 477
  106. def OAI.MUB6.Certificate.PairSemantics.raw7582 line 495
  107. def OAI.MUB6.Certificate.PairSemantics.raw7582step0 line 497
  108. def OAI.MUB6.Certificate.PairSemantics.raw7582step1 line 499
  109. def OAI.MUB6.Certificate.PairSemantics.raw7582step2 line 501
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical7582 line 503
  111. def OAI.MUB6.Certificate.PairSemantics.raw7583 line 520
  112. def OAI.MUB6.Certificate.PairSemantics.raw7583step0 line 522
  113. def OAI.MUB6.Certificate.PairSemantics.raw7583step1 line 524
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical7583 line 526