OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical87.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2784 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw2784step0 line 14
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2784 line 16
  4. def OAI.MUB6.Certificate.PairSemantics.raw2785 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw2785step0 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw2785step1 line 29
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2785 line 31
  8. def OAI.MUB6.Certificate.PairSemantics.raw2786 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw2786step0 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2786 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw2787 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw2787step0 line 59
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2787 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw2788 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw2788step0 line 72
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2788 line 74
  17. def OAI.MUB6.Certificate.PairSemantics.raw2789 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw2789step0 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2789 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw2790 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw2790step0 line 99
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2790 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw2791 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw2791step0 line 113
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2791 line 115
  26. def OAI.MUB6.Certificate.PairSemantics.raw2792 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw2792step0 line 127
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2792 line 129
  29. def OAI.MUB6.Certificate.PairSemantics.raw2793 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw2793step0 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw2793step1 line 143
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2793 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw2794 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw2794step0 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw2794step1 line 163
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2794 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw2795 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw2795step0 line 181
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2795 line 183
  40. def OAI.MUB6.Certificate.PairSemantics.raw2796 line 193
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical2796 line 195
  42. def OAI.MUB6.Certificate.PairSemantics.raw2797 line 199
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2797 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw2798 line 205
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2798 line 207
  46. def OAI.MUB6.Certificate.PairSemantics.raw2799 line 211
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical2799 line 213
  48. def OAI.MUB6.Certificate.PairSemantics.raw2800 line 217
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2800 line 219
  50. def OAI.MUB6.Certificate.PairSemantics.raw2801 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw2801step0 line 225
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2801 line 227
  53. def OAI.MUB6.Certificate.PairSemantics.raw2802 line 236
  54. def OAI.MUB6.Certificate.PairSemantics.raw2802step0 line 238
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2802 line 240
  56. def OAI.MUB6.Certificate.PairSemantics.raw2803 line 249
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2803 line 251
  58. def OAI.MUB6.Certificate.PairSemantics.raw2804 line 255
  59. def OAI.MUB6.Certificate.PairSemantics.raw2804step0 line 257
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2804 line 259
  61. def OAI.MUB6.Certificate.PairSemantics.raw2805 line 268
  62. def OAI.MUB6.Certificate.PairSemantics.raw2805step0 line 270
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2805 line 272
  64. def OAI.MUB6.Certificate.PairSemantics.raw2806 line 282
  65. def OAI.MUB6.Certificate.PairSemantics.raw2806step0 line 284
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2806 line 286
  67. def OAI.MUB6.Certificate.PairSemantics.raw2807 line 295
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical2807 line 297
  69. def OAI.MUB6.Certificate.PairSemantics.raw2808 line 301
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2808 line 303
  71. def OAI.MUB6.Certificate.PairSemantics.raw2809 line 307
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2809 line 309
  73. def OAI.MUB6.Certificate.PairSemantics.raw2810 line 313
  74. def OAI.MUB6.Certificate.PairSemantics.raw2810step0 line 315
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2810 line 317
  76. def OAI.MUB6.Certificate.PairSemantics.raw2811 line 326
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2811 line 328
  78. def OAI.MUB6.Certificate.PairSemantics.raw2812 line 332
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2812 line 334
  80. def OAI.MUB6.Certificate.PairSemantics.raw2813 line 338
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical2813 line 340
  82. def OAI.MUB6.Certificate.PairSemantics.raw2814 line 344
  83. def OAI.MUB6.Certificate.PairSemantics.raw2814step0 line 346
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2814 line 348
  85. def OAI.MUB6.Certificate.PairSemantics.raw2815 line 357
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2815 line 359