OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical86.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2752 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw2752step0 line 13
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2752 line 15
  4. def OAI.MUB6.Certificate.PairSemantics.raw2753 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2753 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw2754 line 30
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2754 line 32
  8. def OAI.MUB6.Certificate.PairSemantics.raw2755 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw2755step0 line 38
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2755 line 40
  11. def OAI.MUB6.Certificate.PairSemantics.raw2756 line 49
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2756 line 51
  13. def OAI.MUB6.Certificate.PairSemantics.raw2757 line 55
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical2757 line 57
  15. def OAI.MUB6.Certificate.PairSemantics.raw2758 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw2758step0 line 63
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2758 line 65
  18. def OAI.MUB6.Certificate.PairSemantics.raw2759 line 74
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2759 line 76
  20. def OAI.MUB6.Certificate.PairSemantics.raw2760 line 80
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2760 line 82
  22. def OAI.MUB6.Certificate.PairSemantics.raw2761 line 86
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2761 line 88
  24. def OAI.MUB6.Certificate.PairSemantics.raw2762 line 92
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2762 line 94
  26. def OAI.MUB6.Certificate.PairSemantics.raw2763 line 98
  27. def OAI.MUB6.Certificate.PairSemantics.raw2763step0 line 100
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2763 line 102
  29. def OAI.MUB6.Certificate.PairSemantics.raw2764 line 111
  30. def OAI.MUB6.Certificate.PairSemantics.raw2764step0 line 113
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2764 line 115
  32. def OAI.MUB6.Certificate.PairSemantics.raw2765 line 124
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2765 line 126
  34. def OAI.MUB6.Certificate.PairSemantics.raw2766 line 130
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical2766 line 132
  36. def OAI.MUB6.Certificate.PairSemantics.raw2767 line 136
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2767 line 138
  38. def OAI.MUB6.Certificate.PairSemantics.raw2768 line 142
  39. def OAI.MUB6.Certificate.PairSemantics.raw2768step0 line 144
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2768 line 146
  41. def OAI.MUB6.Certificate.PairSemantics.raw2769 line 155
  42. def OAI.MUB6.Certificate.PairSemantics.raw2769step0 line 157
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2769 line 159
  44. def OAI.MUB6.Certificate.PairSemantics.raw2770 line 169
  45. def OAI.MUB6.Certificate.PairSemantics.raw2770step0 line 171
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2770 line 173
  47. def OAI.MUB6.Certificate.PairSemantics.raw2771 line 183
  48. def OAI.MUB6.Certificate.PairSemantics.raw2771step0 line 185
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2771 line 187
  50. def OAI.MUB6.Certificate.PairSemantics.raw2772 line 197
  51. def OAI.MUB6.Certificate.PairSemantics.raw2772step0 line 199
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2772 line 201
  53. def OAI.MUB6.Certificate.PairSemantics.raw2773 line 211
  54. def OAI.MUB6.Certificate.PairSemantics.raw2773step0 line 213
  55. def OAI.MUB6.Certificate.PairSemantics.raw2773step1 line 215
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2773 line 217
  57. def OAI.MUB6.Certificate.PairSemantics.raw2774 line 231
  58. def OAI.MUB6.Certificate.PairSemantics.raw2774step0 line 233
  59. def OAI.MUB6.Certificate.PairSemantics.raw2774step1 line 235
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2774 line 237
  61. def OAI.MUB6.Certificate.PairSemantics.raw2775 line 251
  62. def OAI.MUB6.Certificate.PairSemantics.raw2775step0 line 253
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2775 line 255
  64. def OAI.MUB6.Certificate.PairSemantics.raw2776 line 265
  65. def OAI.MUB6.Certificate.PairSemantics.raw2776step0 line 267
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2776 line 269
  67. def OAI.MUB6.Certificate.PairSemantics.raw2777 line 279
  68. def OAI.MUB6.Certificate.PairSemantics.raw2777step0 line 281
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2777 line 283
  70. def OAI.MUB6.Certificate.PairSemantics.raw2778 line 293
  71. def OAI.MUB6.Certificate.PairSemantics.raw2778step0 line 295
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2778 line 297
  73. def OAI.MUB6.Certificate.PairSemantics.raw2779 line 307
  74. def OAI.MUB6.Certificate.PairSemantics.raw2779step0 line 309
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2779 line 311
  76. def OAI.MUB6.Certificate.PairSemantics.raw2780 line 321
  77. def OAI.MUB6.Certificate.PairSemantics.raw2780step0 line 323
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2780 line 325
  79. def OAI.MUB6.Certificate.PairSemantics.raw2781 line 335
  80. def OAI.MUB6.Certificate.PairSemantics.raw2781step0 line 337
  81. def OAI.MUB6.Certificate.PairSemantics.raw2781step1 line 339
  82. def OAI.MUB6.Certificate.PairSemantics.raw2781step2 line 341
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2781 line 343
  84. def OAI.MUB6.Certificate.PairSemantics.raw2782 line 361
  85. def OAI.MUB6.Certificate.PairSemantics.raw2782step0 line 363
  86. def OAI.MUB6.Certificate.PairSemantics.raw2782step1 line 365
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2782 line 367
  88. def OAI.MUB6.Certificate.PairSemantics.raw2783 line 381
  89. def OAI.MUB6.Certificate.PairSemantics.raw2783step0 line 383
  90. def OAI.MUB6.Certificate.PairSemantics.raw2783step1 line 385
  91. def OAI.MUB6.Certificate.PairSemantics.raw2783step2 line 387
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2783 line 389