OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical302.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9664 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw9664step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw9664step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9664 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw9665 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw9665step0 line 41
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical9665 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw9666 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw9666step0 line 54
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9666 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw9667 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw9667step0 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9667 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw9668 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw9668step0 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw9668step1 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9668 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw9669 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw9669step0 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical9669 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw9670 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw9670step0 line 112
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9670 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw9671 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw9671step0 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw9671step1 line 127
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9671 line 129
  28. def OAI.MUB6.Certificate.PairSemantics.raw9672 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw9672step0 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw9672step1 line 146
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9672 line 148
  32. def OAI.MUB6.Certificate.PairSemantics.raw9673 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw9673step0 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw9673step1 line 165
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9673 line 167
  36. def OAI.MUB6.Certificate.PairSemantics.raw9674 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw9674step0 line 182
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9674 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw9675 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw9675step0 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw9675step1 line 197
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9675 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw9676 line 212
  44. def OAI.MUB6.Certificate.PairSemantics.raw9676step0 line 214
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9676 line 216
  46. def OAI.MUB6.Certificate.PairSemantics.raw9677 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw9677step0 line 227
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9677 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw9678 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw9678step0 line 240
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical9678 line 242
  52. def OAI.MUB6.Certificate.PairSemantics.raw9679 line 251
  53. def OAI.MUB6.Certificate.PairSemantics.raw9679step0 line 253
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9679 line 255
  55. def OAI.MUB6.Certificate.PairSemantics.raw9680 line 264
  56. def OAI.MUB6.Certificate.PairSemantics.raw9680step0 line 266
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9680 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw9681 line 277
  59. def OAI.MUB6.Certificate.PairSemantics.raw9681step0 line 279
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical9681 line 281
  61. def OAI.MUB6.Certificate.PairSemantics.raw9682 line 290
  62. def OAI.MUB6.Certificate.PairSemantics.raw9682step0 line 292
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9682 line 294
  64. def OAI.MUB6.Certificate.PairSemantics.raw9683 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw9683step0 line 305
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9683 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw9684 line 316
  68. def OAI.MUB6.Certificate.PairSemantics.raw9684step0 line 318
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9684 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw9685 line 329
  71. def OAI.MUB6.Certificate.PairSemantics.raw9685step0 line 331
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9685 line 333
  73. def OAI.MUB6.Certificate.PairSemantics.raw9686 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw9686step0 line 344
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9686 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw9687 line 355
  77. def OAI.MUB6.Certificate.PairSemantics.raw9687step0 line 357
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9687 line 359
  79. def OAI.MUB6.Certificate.PairSemantics.raw9688 line 368
  80. def OAI.MUB6.Certificate.PairSemantics.raw9688step0 line 370
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9688 line 372
  82. def OAI.MUB6.Certificate.PairSemantics.raw9689 line 381
  83. def OAI.MUB6.Certificate.PairSemantics.raw9689step0 line 383
  84. def OAI.MUB6.Certificate.PairSemantics.raw9689step1 line 385
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9689 line 387
  86. def OAI.MUB6.Certificate.PairSemantics.raw9690 line 400
  87. def OAI.MUB6.Certificate.PairSemantics.raw9690step0 line 402
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9690 line 404
  89. def OAI.MUB6.Certificate.PairSemantics.raw9691 line 413
  90. def OAI.MUB6.Certificate.PairSemantics.raw9691step0 line 415
  91. def OAI.MUB6.Certificate.PairSemantics.raw9691step1 line 417
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9691 line 419
  93. def OAI.MUB6.Certificate.PairSemantics.raw9692 line 433
  94. def OAI.MUB6.Certificate.PairSemantics.raw9692step0 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw9692step1 line 437
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9692 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw9693 line 453
  98. def OAI.MUB6.Certificate.PairSemantics.raw9693step0 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw9693step1 line 457
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9693 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw9694 line 473
  102. def OAI.MUB6.Certificate.PairSemantics.raw9694step0 line 475
  103. def OAI.MUB6.Certificate.PairSemantics.raw9694step1 line 477
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical9694 line 479
  105. def OAI.MUB6.Certificate.PairSemantics.raw9695 line 493
  106. def OAI.MUB6.Certificate.PairSemantics.raw9695step0 line 495
  107. def OAI.MUB6.Certificate.PairSemantics.raw9695step1 line 497
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical9695 line 499