OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical84.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2688 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw2688step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2688 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw2689 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw2689step0 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw2689step1 line 31
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2689 line 33
  8. def OAI.MUB6.Certificate.PairSemantics.raw2690 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw2690step0 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw2690step1 line 50
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2690 line 52
  12. def OAI.MUB6.Certificate.PairSemantics.raw2691 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw2691step0 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw2691step1 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2691 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw2692 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw2692step0 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw2692step1 line 88
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2692 line 90
  20. def OAI.MUB6.Certificate.PairSemantics.raw2693 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw2693step0 line 105
  22. def OAI.MUB6.Certificate.PairSemantics.raw2693step1 line 107
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2693 line 109
  24. def OAI.MUB6.Certificate.PairSemantics.raw2694 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2694 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw2695 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw2695step0 line 130
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2695 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw2696 line 141
  30. def OAI.MUB6.Certificate.PairSemantics.raw2696step0 line 143
  31. def OAI.MUB6.Certificate.PairSemantics.raw2696step1 line 145
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2696 line 147
  33. def OAI.MUB6.Certificate.PairSemantics.raw2697 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw2697step0 line 162
  35. def OAI.MUB6.Certificate.PairSemantics.raw2697step1 line 164
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2697 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw2698 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw2698step0 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw2698step1 line 183
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2698 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw2699 line 198
  42. def OAI.MUB6.Certificate.PairSemantics.raw2699step0 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw2699step1 line 202
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2699 line 204
  45. def OAI.MUB6.Certificate.PairSemantics.raw2700 line 217
  46. def OAI.MUB6.Certificate.PairSemantics.raw2700step0 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw2700step1 line 221
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2700 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw2701 line 236
  50. def OAI.MUB6.Certificate.PairSemantics.raw2701step0 line 238
  51. def OAI.MUB6.Certificate.PairSemantics.raw2701step1 line 240
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2701 line 242
  53. def OAI.MUB6.Certificate.PairSemantics.raw2702 line 255
  54. def OAI.MUB6.Certificate.PairSemantics.raw2702step0 line 257
  55. def OAI.MUB6.Certificate.PairSemantics.raw2702step1 line 259
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2702 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw2703 line 274
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical2703 line 276
  59. def OAI.MUB6.Certificate.PairSemantics.raw2704 line 280
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2704 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw2705 line 286
  62. def OAI.MUB6.Certificate.PairSemantics.raw2705step0 line 288
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2705 line 290
  64. def OAI.MUB6.Certificate.PairSemantics.raw2706 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw2706step0 line 301
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2706 line 303
  67. def OAI.MUB6.Certificate.PairSemantics.raw2707 line 312
  68. def OAI.MUB6.Certificate.PairSemantics.raw2707step0 line 314
  69. def OAI.MUB6.Certificate.PairSemantics.raw2707step1 line 316
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2707 line 318
  71. def OAI.MUB6.Certificate.PairSemantics.raw2708 line 331
  72. def OAI.MUB6.Certificate.PairSemantics.raw2708step0 line 333
  73. def OAI.MUB6.Certificate.PairSemantics.raw2708step1 line 335
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2708 line 337
  75. def OAI.MUB6.Certificate.PairSemantics.raw2709 line 350
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2709 line 352
  77. def OAI.MUB6.Certificate.PairSemantics.raw2710 line 356
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2710 line 358
  79. def OAI.MUB6.Certificate.PairSemantics.raw2711 line 362
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2711 line 364
  81. def OAI.MUB6.Certificate.PairSemantics.raw2712 line 368
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2712 line 370
  83. def OAI.MUB6.Certificate.PairSemantics.raw2713 line 374
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2713 line 376
  85. def OAI.MUB6.Certificate.PairSemantics.raw2714 line 380
  86. def OAI.MUB6.Certificate.PairSemantics.raw2714step0 line 382
  87. def OAI.MUB6.Certificate.PairSemantics.raw2714step1 line 384
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2714 line 386
  89. def OAI.MUB6.Certificate.PairSemantics.raw2715 line 399
  90. def OAI.MUB6.Certificate.PairSemantics.raw2715step0 line 401
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical2715 line 403
  92. def OAI.MUB6.Certificate.PairSemantics.raw2716 line 412
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical2716 line 414
  94. def OAI.MUB6.Certificate.PairSemantics.raw2717 line 418
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical2717 line 420
  96. def OAI.MUB6.Certificate.PairSemantics.raw2718 line 424
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2718 line 426
  98. def OAI.MUB6.Certificate.PairSemantics.raw2719 line 430
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical2719 line 432