OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical83.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2656 line 15
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2656 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw2657 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw2657step0 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw2657step1 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2657 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw2658 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw2658step0 line 42
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2658 line 44
  10. def OAI.MUB6.Certificate.PairSemantics.raw2659 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw2659step0 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2659 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw2660 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw2660step0 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw2660step1 line 70
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2660 line 72
  17. def OAI.MUB6.Certificate.PairSemantics.raw2661 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw2661step0 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw2661step1 line 89
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical2661 line 91
  21. def OAI.MUB6.Certificate.PairSemantics.raw2662 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw2662step0 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw2662step1 line 108
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2662 line 110
  25. def OAI.MUB6.Certificate.PairSemantics.raw2663 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw2663step0 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw2663step1 line 127
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2663 line 129
  29. def OAI.MUB6.Certificate.PairSemantics.raw2664 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw2664step0 line 144
  31. def OAI.MUB6.Certificate.PairSemantics.raw2664step1 line 146
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2664 line 148
  33. def OAI.MUB6.Certificate.PairSemantics.raw2665 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw2665step0 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw2665step1 line 165
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2665 line 167
  37. def OAI.MUB6.Certificate.PairSemantics.raw2666 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw2666step0 line 182
  39. def OAI.MUB6.Certificate.PairSemantics.raw2666step1 line 184
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2666 line 186
  41. def OAI.MUB6.Certificate.PairSemantics.raw2667 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw2667step0 line 201
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2667 line 203
  44. def OAI.MUB6.Certificate.PairSemantics.raw2668 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw2668step0 line 214
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2668 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw2669 line 225
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2669 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw2670 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw2670step0 line 233
  51. def OAI.MUB6.Certificate.PairSemantics.raw2670step1 line 235
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2670 line 237
  53. def OAI.MUB6.Certificate.PairSemantics.raw2671 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw2671step0 line 252
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2671 line 254
  56. def OAI.MUB6.Certificate.PairSemantics.raw2672 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw2672step0 line 265
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical2672 line 267
  59. def OAI.MUB6.Certificate.PairSemantics.raw2673 line 276
  60. def OAI.MUB6.Certificate.PairSemantics.raw2673step0 line 278
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2673 line 280
  62. def OAI.MUB6.Certificate.PairSemantics.raw2674 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw2674step0 line 291
  64. def OAI.MUB6.Certificate.PairSemantics.raw2674step1 line 293
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2674 line 295
  66. def OAI.MUB6.Certificate.PairSemantics.raw2675 line 308
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2675 line 310
  68. def OAI.MUB6.Certificate.PairSemantics.raw2676 line 314
  69. def OAI.MUB6.Certificate.PairSemantics.raw2676step0 line 316
  70. def OAI.MUB6.Certificate.PairSemantics.raw2676step1 line 318
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2676 line 320
  72. def OAI.MUB6.Certificate.PairSemantics.raw2677 line 333
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical2677 line 335
  74. def OAI.MUB6.Certificate.PairSemantics.raw2678 line 339
  75. def OAI.MUB6.Certificate.PairSemantics.raw2678step0 line 341
  76. def OAI.MUB6.Certificate.PairSemantics.raw2678step1 line 343
  77. def OAI.MUB6.Certificate.PairSemantics.raw2678step2 line 345
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2678 line 347
  79. def OAI.MUB6.Certificate.PairSemantics.raw2679 line 365
  80. def OAI.MUB6.Certificate.PairSemantics.raw2679step0 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw2679step1 line 369
  82. def OAI.MUB6.Certificate.PairSemantics.raw2679step2 line 371
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2679 line 373
  84. def OAI.MUB6.Certificate.PairSemantics.raw2680 line 391
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical2680 line 393
  86. def OAI.MUB6.Certificate.PairSemantics.raw2681 line 397
  87. def OAI.MUB6.Certificate.PairSemantics.raw2681step0 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw2681step1 line 401
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2681 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw2682 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw2682step0 line 418
  92. def OAI.MUB6.Certificate.PairSemantics.raw2682step1 line 420
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical2682 line 422
  94. def OAI.MUB6.Certificate.PairSemantics.raw2683 line 435
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical2683 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw2684 line 441
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2684 line 443
  98. def OAI.MUB6.Certificate.PairSemantics.raw2685 line 447
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical2685 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw2686 line 453
  101. def OAI.MUB6.Certificate.PairSemantics.raw2686step0 line 455
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical2686 line 457
  103. def OAI.MUB6.Certificate.PairSemantics.raw2687 line 466
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical2687 line 468