OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical239.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7648 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw7648step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical7648 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw7649 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw7649step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical7649 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw7650 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw7650step0 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw7650step1 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7650 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw7651 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw7651step0 line 62
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7651 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw7652 line 73
  15. def OAI.MUB6.Certificate.PairSemantics.raw7652step0 line 75
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7652 line 77
  17. def OAI.MUB6.Certificate.PairSemantics.raw7653 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw7653step0 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw7653step1 line 90
  20. def OAI.MUB6.Certificate.PairSemantics.raw7653step2 line 92
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7653 line 94
  22. def OAI.MUB6.Certificate.PairSemantics.raw7654 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7654step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw7654step1 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7654 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw7655 line 133
  27. def OAI.MUB6.Certificate.PairSemantics.raw7655step0 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw7655step1 line 137
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical7655 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw7656 line 153
  31. def OAI.MUB6.Certificate.PairSemantics.raw7656step0 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw7656step1 line 157
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7656 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw7657 line 173
  35. def OAI.MUB6.Certificate.PairSemantics.raw7657step0 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw7657step1 line 177
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical7657 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw7658 line 193
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7658 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw7659 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw7659step0 line 201
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7659 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw7660 line 212
  44. def OAI.MUB6.Certificate.PairSemantics.raw7660step0 line 214
  45. def OAI.MUB6.Certificate.PairSemantics.raw7660step1 line 216
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical7660 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw7661 line 232
  48. def OAI.MUB6.Certificate.PairSemantics.raw7661step0 line 234
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical7661 line 236
  50. def OAI.MUB6.Certificate.PairSemantics.raw7662 line 245
  51. def OAI.MUB6.Certificate.PairSemantics.raw7662step0 line 247
  52. def OAI.MUB6.Certificate.PairSemantics.raw7662step1 line 249
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical7662 line 251
  54. def OAI.MUB6.Certificate.PairSemantics.raw7663 line 265
  55. def OAI.MUB6.Certificate.PairSemantics.raw7663step0 line 267
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical7663 line 269
  57. def OAI.MUB6.Certificate.PairSemantics.raw7664 line 278
  58. def OAI.MUB6.Certificate.PairSemantics.raw7664step0 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw7664step1 line 282
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical7664 line 284
  61. def OAI.MUB6.Certificate.PairSemantics.raw7665 line 298
  62. def OAI.MUB6.Certificate.PairSemantics.raw7665step0 line 300
  63. def OAI.MUB6.Certificate.PairSemantics.raw7665step1 line 302
  64. def OAI.MUB6.Certificate.PairSemantics.raw7665step2 line 304
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7665 line 306
  66. def OAI.MUB6.Certificate.PairSemantics.raw7666 line 325
  67. def OAI.MUB6.Certificate.PairSemantics.raw7666step0 line 327
  68. def OAI.MUB6.Certificate.PairSemantics.raw7666step1 line 329
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7666 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw7667 line 345
  71. def OAI.MUB6.Certificate.PairSemantics.raw7667step0 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw7667step1 line 349
  73. def OAI.MUB6.Certificate.PairSemantics.raw7667step2 line 351
  74. def OAI.MUB6.Certificate.PairSemantics.raw7667step3 line 353
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7667 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw7668 line 379
  77. def OAI.MUB6.Certificate.PairSemantics.raw7668step0 line 381
  78. def OAI.MUB6.Certificate.PairSemantics.raw7668step1 line 383
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical7668 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw7669 line 400
  81. def OAI.MUB6.Certificate.PairSemantics.raw7669step0 line 402
  82. def OAI.MUB6.Certificate.PairSemantics.raw7669step1 line 404
  83. def OAI.MUB6.Certificate.PairSemantics.raw7669step2 line 406
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7669 line 408
  85. def OAI.MUB6.Certificate.PairSemantics.raw7670 line 427
  86. def OAI.MUB6.Certificate.PairSemantics.raw7670step0 line 429
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7670 line 431
  88. def OAI.MUB6.Certificate.PairSemantics.raw7671 line 441
  89. def OAI.MUB6.Certificate.PairSemantics.raw7671step0 line 443
  90. def OAI.MUB6.Certificate.PairSemantics.raw7671step1 line 445
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7671 line 447
  92. def OAI.MUB6.Certificate.PairSemantics.raw7672 line 461
  93. def OAI.MUB6.Certificate.PairSemantics.raw7672step0 line 463
  94. def OAI.MUB6.Certificate.PairSemantics.raw7672step1 line 465
  95. def OAI.MUB6.Certificate.PairSemantics.raw7672step2 line 467
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7672 line 469
  97. def OAI.MUB6.Certificate.PairSemantics.raw7673 line 488
  98. def OAI.MUB6.Certificate.PairSemantics.raw7673step0 line 490
  99. def OAI.MUB6.Certificate.PairSemantics.raw7673step1 line 492
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical7673 line 494
  101. def OAI.MUB6.Certificate.PairSemantics.raw7674 line 508
  102. def OAI.MUB6.Certificate.PairSemantics.raw7674step0 line 510
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7674 line 512
  104. def OAI.MUB6.Certificate.PairSemantics.raw7675 line 521
  105. def OAI.MUB6.Certificate.PairSemantics.raw7675step0 line 523
  106. def OAI.MUB6.Certificate.PairSemantics.raw7675step1 line 525
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7675 line 527
  108. def OAI.MUB6.Certificate.PairSemantics.raw7676 line 541
  109. def OAI.MUB6.Certificate.PairSemantics.raw7676step0 line 543
  110. def OAI.MUB6.Certificate.PairSemantics.raw7676step1 line 545
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical7676 line 547
  112. def OAI.MUB6.Certificate.PairSemantics.raw7677 line 562
  113. def OAI.MUB6.Certificate.PairSemantics.raw7677step0 line 564
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical7677 line 566
  115. def OAI.MUB6.Certificate.PairSemantics.raw7678 line 576
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7678 line 578
  117. def OAI.MUB6.Certificate.PairSemantics.raw7679 line 582
  118. def OAI.MUB6.Certificate.PairSemantics.raw7679step0 line 584
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical7679 line 586