OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical85.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2720 line 12
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2720 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw2721 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2721 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw2722 line 24
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2722 line 26
  7. def OAI.MUB6.Certificate.PairSemantics.raw2723 line 30
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2723 line 32
  9. def OAI.MUB6.Certificate.PairSemantics.raw2724 line 36
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2724 line 38
  11. def OAI.MUB6.Certificate.PairSemantics.raw2725 line 42
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2725 line 44
  13. def OAI.MUB6.Certificate.PairSemantics.raw2726 line 48
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical2726 line 50
  15. def OAI.MUB6.Certificate.PairSemantics.raw2727 line 54
  16. def OAI.MUB6.Certificate.PairSemantics.raw2727step0 line 56
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2727 line 58
  18. def OAI.MUB6.Certificate.PairSemantics.raw2728 line 67
  19. def OAI.MUB6.Certificate.PairSemantics.raw2728step0 line 69
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical2728 line 71
  21. def OAI.MUB6.Certificate.PairSemantics.raw2729 line 80
  22. def OAI.MUB6.Certificate.PairSemantics.raw2729step0 line 82
  23. def OAI.MUB6.Certificate.PairSemantics.raw2729step1 line 84
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2729 line 86
  25. def OAI.MUB6.Certificate.PairSemantics.raw2730 line 99
  26. def OAI.MUB6.Certificate.PairSemantics.raw2730step0 line 101
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2730 line 103
  28. def OAI.MUB6.Certificate.PairSemantics.raw2731 line 112
  29. def OAI.MUB6.Certificate.PairSemantics.raw2731step0 line 114
  30. def OAI.MUB6.Certificate.PairSemantics.raw2731step1 line 116
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2731 line 118
  32. def OAI.MUB6.Certificate.PairSemantics.raw2732 line 131
  33. def OAI.MUB6.Certificate.PairSemantics.raw2732step0 line 133
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2732 line 135
  35. def OAI.MUB6.Certificate.PairSemantics.raw2733 line 144
  36. def OAI.MUB6.Certificate.PairSemantics.raw2733step0 line 146
  37. def OAI.MUB6.Certificate.PairSemantics.raw2733step1 line 148
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical2733 line 150
  39. def OAI.MUB6.Certificate.PairSemantics.raw2734 line 163
  40. def OAI.MUB6.Certificate.PairSemantics.raw2734step0 line 165
  41. def OAI.MUB6.Certificate.PairSemantics.raw2734step1 line 167
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2734 line 169
  43. def OAI.MUB6.Certificate.PairSemantics.raw2735 line 182
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2735 line 184
  45. def OAI.MUB6.Certificate.PairSemantics.raw2736 line 188
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2736 line 190
  47. def OAI.MUB6.Certificate.PairSemantics.raw2737 line 194
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2737 line 196
  49. def OAI.MUB6.Certificate.PairSemantics.raw2738 line 200
  50. def OAI.MUB6.Certificate.PairSemantics.raw2738step0 line 202
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2738 line 204
  52. def OAI.MUB6.Certificate.PairSemantics.raw2739 line 214
  53. def OAI.MUB6.Certificate.PairSemantics.raw2739step0 line 216
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2739 line 218
  55. def OAI.MUB6.Certificate.PairSemantics.raw2740 line 228
  56. def OAI.MUB6.Certificate.PairSemantics.raw2740step0 line 230
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2740 line 232
  58. def OAI.MUB6.Certificate.PairSemantics.raw2741 line 242
  59. def OAI.MUB6.Certificate.PairSemantics.raw2741step0 line 244
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2741 line 246
  61. def OAI.MUB6.Certificate.PairSemantics.raw2742 line 256
  62. def OAI.MUB6.Certificate.PairSemantics.raw2742step0 line 258
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2742 line 260
  64. def OAI.MUB6.Certificate.PairSemantics.raw2743 line 270
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2743 line 272
  66. def OAI.MUB6.Certificate.PairSemantics.raw2744 line 276
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2744 line 278
  68. def OAI.MUB6.Certificate.PairSemantics.raw2745 line 282
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2745 line 284
  70. def OAI.MUB6.Certificate.PairSemantics.raw2746 line 288
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2746 line 290
  72. def OAI.MUB6.Certificate.PairSemantics.raw2747 line 294
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical2747 line 296
  74. def OAI.MUB6.Certificate.PairSemantics.raw2748 line 300
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2748 line 302
  76. def OAI.MUB6.Certificate.PairSemantics.raw2749 line 306
  77. def OAI.MUB6.Certificate.PairSemantics.raw2749step0 line 308
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2749 line 310
  79. def OAI.MUB6.Certificate.PairSemantics.raw2750 line 319
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2750 line 321
  81. def OAI.MUB6.Certificate.PairSemantics.raw2751 line 325
  82. def OAI.MUB6.Certificate.PairSemantics.raw2751step0 line 327
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2751 line 329