OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical91.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2912 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw2912step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw2912step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2912 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw2913 line 38
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2913 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw2914 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw2914step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2914 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw2915 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw2915step0 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2915 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw2916 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw2916step0 line 72
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2916 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw2917 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2917 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw2918 line 89
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2918 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw2919 line 95
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2919 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw2920 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw2920step0 line 103
  24. def OAI.MUB6.Certificate.PairSemantics.raw2920step1 line 105
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2920 line 107
  26. def OAI.MUB6.Certificate.PairSemantics.raw2921 line 120
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2921 line 122
  28. def OAI.MUB6.Certificate.PairSemantics.raw2922 line 126
  29. def OAI.MUB6.Certificate.PairSemantics.raw2922step0 line 128
  30. def OAI.MUB6.Certificate.PairSemantics.raw2922step1 line 130
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2922 line 132
  32. def OAI.MUB6.Certificate.PairSemantics.raw2923 line 145
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2923 line 147
  34. def OAI.MUB6.Certificate.PairSemantics.raw2924 line 151
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical2924 line 153
  36. def OAI.MUB6.Certificate.PairSemantics.raw2925 line 157
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2925 line 159
  38. def OAI.MUB6.Certificate.PairSemantics.raw2926 line 163
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2926 line 165
  40. def OAI.MUB6.Certificate.PairSemantics.raw2927 line 169
  41. def OAI.MUB6.Certificate.PairSemantics.raw2927step0 line 171
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2927 line 173
  43. def OAI.MUB6.Certificate.PairSemantics.raw2928 line 182
  44. def OAI.MUB6.Certificate.PairSemantics.raw2928step0 line 184
  45. def OAI.MUB6.Certificate.PairSemantics.raw2928step1 line 186
  46. def OAI.MUB6.Certificate.PairSemantics.raw2928step2 line 188
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical2928 line 190
  48. def OAI.MUB6.Certificate.PairSemantics.raw2929 line 207
  49. def OAI.MUB6.Certificate.PairSemantics.raw2929step0 line 209
  50. def OAI.MUB6.Certificate.PairSemantics.raw2929step1 line 211
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2929 line 213
  52. def OAI.MUB6.Certificate.PairSemantics.raw2930 line 226
  53. def OAI.MUB6.Certificate.PairSemantics.raw2930step0 line 228
  54. def OAI.MUB6.Certificate.PairSemantics.raw2930step1 line 230
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2930 line 232
  56. def OAI.MUB6.Certificate.PairSemantics.raw2931 line 245
  57. def OAI.MUB6.Certificate.PairSemantics.raw2931step0 line 247
  58. def OAI.MUB6.Certificate.PairSemantics.raw2931step1 line 249
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2931 line 251
  60. def OAI.MUB6.Certificate.PairSemantics.raw2932 line 264
  61. def OAI.MUB6.Certificate.PairSemantics.raw2932step0 line 266
  62. def OAI.MUB6.Certificate.PairSemantics.raw2932step1 line 268
  63. def OAI.MUB6.Certificate.PairSemantics.raw2932step2 line 270
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2932 line 272
  65. def OAI.MUB6.Certificate.PairSemantics.raw2933 line 289
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2933 line 291
  67. def OAI.MUB6.Certificate.PairSemantics.raw2934 line 295
  68. def OAI.MUB6.Certificate.PairSemantics.raw2934step0 line 297
  69. def OAI.MUB6.Certificate.PairSemantics.raw2934step1 line 299
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2934 line 301
  71. def OAI.MUB6.Certificate.PairSemantics.raw2935 line 314
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2935 line 316
  73. def OAI.MUB6.Certificate.PairSemantics.raw2936 line 320
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2936 line 322
  75. def OAI.MUB6.Certificate.PairSemantics.raw2937 line 326
  76. def OAI.MUB6.Certificate.PairSemantics.raw2937step0 line 328
  77. def OAI.MUB6.Certificate.PairSemantics.raw2937step1 line 330
  78. def OAI.MUB6.Certificate.PairSemantics.raw2937step2 line 332
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2937 line 334
  80. def OAI.MUB6.Certificate.PairSemantics.raw2938 line 351
  81. def OAI.MUB6.Certificate.PairSemantics.raw2938step0 line 353
  82. def OAI.MUB6.Certificate.PairSemantics.raw2938step1 line 355
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2938 line 357
  84. def OAI.MUB6.Certificate.PairSemantics.raw2939 line 370
  85. def OAI.MUB6.Certificate.PairSemantics.raw2939step0 line 372
  86. def OAI.MUB6.Certificate.PairSemantics.raw2939step1 line 374
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2939 line 376
  88. def OAI.MUB6.Certificate.PairSemantics.raw2940 line 389
  89. def OAI.MUB6.Certificate.PairSemantics.raw2940step0 line 391
  90. def OAI.MUB6.Certificate.PairSemantics.raw2940step1 line 393
  91. def OAI.MUB6.Certificate.PairSemantics.raw2940step2 line 395
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2940 line 397
  93. def OAI.MUB6.Certificate.PairSemantics.raw2941 line 415
  94. def OAI.MUB6.Certificate.PairSemantics.raw2941step0 line 417
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical2941 line 419
  96. def OAI.MUB6.Certificate.PairSemantics.raw2942 line 428
  97. def OAI.MUB6.Certificate.PairSemantics.raw2942step0 line 430
  98. def OAI.MUB6.Certificate.PairSemantics.raw2942step1 line 432
  99. def OAI.MUB6.Certificate.PairSemantics.raw2942step2 line 434
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical2942 line 436
  101. def OAI.MUB6.Certificate.PairSemantics.raw2943 line 454
  102. def OAI.MUB6.Certificate.PairSemantics.raw2943step0 line 456
  103. def OAI.MUB6.Certificate.PairSemantics.raw2943step1 line 458
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical2943 line 460