OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical143.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4576 line 21
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4576 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw4577 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw4577step0 line 29
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4577 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw4578 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw4578step0 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw4578step1 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4578 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw4579 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw4579step0 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw4579step1 line 63
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4579 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw4580 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw4580step0 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw4580step1 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4580 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw4581 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw4581step0 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4581 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw4582 line 110
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4582 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw4583 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw4583step0 line 118
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4583 line 120
  26. def OAI.MUB6.Certificate.PairSemantics.raw4584 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw4584step0 line 131
  28. def OAI.MUB6.Certificate.PairSemantics.raw4584step1 line 133
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4584 line 135
  30. def OAI.MUB6.Certificate.PairSemantics.raw4585 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw4585step0 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw4585step1 line 152
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4585 line 154
  34. def OAI.MUB6.Certificate.PairSemantics.raw4586 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw4586step0 line 169
  36. def OAI.MUB6.Certificate.PairSemantics.raw4586step1 line 171
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4586 line 173
  38. def OAI.MUB6.Certificate.PairSemantics.raw4587 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw4587step0 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw4587step1 line 190
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical4587 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw4588 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw4588step0 line 207
  44. def OAI.MUB6.Certificate.PairSemantics.raw4588step1 line 209
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical4588 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw4589 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw4589step0 line 226
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4589 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw4590 line 237
  50. def OAI.MUB6.Certificate.PairSemantics.raw4590step0 line 239
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4590 line 241
  52. def OAI.MUB6.Certificate.PairSemantics.raw4591 line 250
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4591 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw4592 line 256
  55. def OAI.MUB6.Certificate.PairSemantics.raw4592step0 line 258
  56. def OAI.MUB6.Certificate.PairSemantics.raw4592step1 line 260
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4592 line 262
  58. def OAI.MUB6.Certificate.PairSemantics.raw4593 line 275
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4593 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw4594 line 281
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4594 line 283
  62. def OAI.MUB6.Certificate.PairSemantics.raw4595 line 287
  63. def OAI.MUB6.Certificate.PairSemantics.raw4595step0 line 289
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4595 line 291
  65. def OAI.MUB6.Certificate.PairSemantics.raw4596 line 300
  66. def OAI.MUB6.Certificate.PairSemantics.raw4596step0 line 302
  67. def OAI.MUB6.Certificate.PairSemantics.raw4596step1 line 304
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical4596 line 306
  69. def OAI.MUB6.Certificate.PairSemantics.raw4597 line 319
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4597 line 321
  71. def OAI.MUB6.Certificate.PairSemantics.raw4598 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4598 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw4599 line 331
  74. def OAI.MUB6.Certificate.PairSemantics.raw4599step0 line 333
  75. def OAI.MUB6.Certificate.PairSemantics.raw4599step1 line 335
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4599 line 337
  77. def OAI.MUB6.Certificate.PairSemantics.raw4600 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw4600step0 line 352
  79. def OAI.MUB6.Certificate.PairSemantics.raw4600step1 line 354
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4600 line 356
  81. def OAI.MUB6.Certificate.PairSemantics.raw4601 line 369
  82. def OAI.MUB6.Certificate.PairSemantics.raw4601step0 line 371
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4601 line 373
  84. def OAI.MUB6.Certificate.PairSemantics.raw4602 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw4602step0 line 384
  86. def OAI.MUB6.Certificate.PairSemantics.raw4602step1 line 386
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4602 line 388
  88. def OAI.MUB6.Certificate.PairSemantics.raw4603 line 401
  89. def OAI.MUB6.Certificate.PairSemantics.raw4603step0 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw4603step1 line 405
  91. def OAI.MUB6.Certificate.PairSemantics.raw4603step2 line 407
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical4603 line 409
  93. def OAI.MUB6.Certificate.PairSemantics.raw4604 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw4604step0 line 428
  95. def OAI.MUB6.Certificate.PairSemantics.raw4604step1 line 430
  96. def OAI.MUB6.Certificate.PairSemantics.raw4604step2 line 432
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4604 line 434
  98. def OAI.MUB6.Certificate.PairSemantics.raw4605 line 451
  99. def OAI.MUB6.Certificate.PairSemantics.raw4605step0 line 453
  100. def OAI.MUB6.Certificate.PairSemantics.raw4605step1 line 455
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4605 line 457
  102. def OAI.MUB6.Certificate.PairSemantics.raw4606 line 470
  103. def OAI.MUB6.Certificate.PairSemantics.raw4606step0 line 472
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4606 line 474
  105. def OAI.MUB6.Certificate.PairSemantics.raw4607 line 483
  106. def OAI.MUB6.Certificate.PairSemantics.raw4607step0 line 485
  107. def OAI.MUB6.Certificate.PairSemantics.raw4607step1 line 487
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4607 line 489