OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical63.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2016 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2016 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw2017 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw2017step0 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw2017step1 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2017 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw2018 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2018 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw2019 line 47
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2019 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw2020 line 53
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2020 line 55
  13. def OAI.MUB6.Certificate.PairSemantics.raw2021 line 59
  14. def OAI.MUB6.Certificate.PairSemantics.raw2021step0 line 61
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2021 line 63
  16. def OAI.MUB6.Certificate.PairSemantics.raw2022 line 72
  17. def OAI.MUB6.Certificate.PairSemantics.raw2022step0 line 74
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2022 line 76
  19. def OAI.MUB6.Certificate.PairSemantics.raw2023 line 85
  20. def OAI.MUB6.Certificate.PairSemantics.raw2023step0 line 87
  21. def OAI.MUB6.Certificate.PairSemantics.raw2023step1 line 89
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2023 line 91
  23. def OAI.MUB6.Certificate.PairSemantics.raw2024 line 104
  24. def OAI.MUB6.Certificate.PairSemantics.raw2024step0 line 106
  25. def OAI.MUB6.Certificate.PairSemantics.raw2024step1 line 108
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical2024 line 110
  27. def OAI.MUB6.Certificate.PairSemantics.raw2025 line 123
  28. def OAI.MUB6.Certificate.PairSemantics.raw2025step0 line 125
  29. def OAI.MUB6.Certificate.PairSemantics.raw2025step1 line 127
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2025 line 129
  31. def OAI.MUB6.Certificate.PairSemantics.raw2026 line 142
  32. def OAI.MUB6.Certificate.PairSemantics.raw2026step0 line 144
  33. def OAI.MUB6.Certificate.PairSemantics.raw2026step1 line 146
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2026 line 148
  35. def OAI.MUB6.Certificate.PairSemantics.raw2027 line 161
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2027 line 163
  37. def OAI.MUB6.Certificate.PairSemantics.raw2028 line 167
  38. def OAI.MUB6.Certificate.PairSemantics.raw2028step0 line 169
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2028 line 171
  40. def OAI.MUB6.Certificate.PairSemantics.raw2029 line 180
  41. def OAI.MUB6.Certificate.PairSemantics.raw2029step0 line 182
  42. def OAI.MUB6.Certificate.PairSemantics.raw2029step1 line 184
  43. def OAI.MUB6.Certificate.PairSemantics.raw2029step2 line 186
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2029 line 188
  45. def OAI.MUB6.Certificate.PairSemantics.raw2030 line 205
  46. def OAI.MUB6.Certificate.PairSemantics.raw2030step0 line 207
  47. def OAI.MUB6.Certificate.PairSemantics.raw2030step1 line 209
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2030 line 211
  49. def OAI.MUB6.Certificate.PairSemantics.raw2031 line 224
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical2031 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw2032 line 230
  52. def OAI.MUB6.Certificate.PairSemantics.raw2032step0 line 232
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2032 line 234
  54. def OAI.MUB6.Certificate.PairSemantics.raw2033 line 243
  55. def OAI.MUB6.Certificate.PairSemantics.raw2033step0 line 245
  56. def OAI.MUB6.Certificate.PairSemantics.raw2033step1 line 247
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2033 line 249
  58. def OAI.MUB6.Certificate.PairSemantics.raw2034 line 262
  59. def OAI.MUB6.Certificate.PairSemantics.raw2034step0 line 264
  60. def OAI.MUB6.Certificate.PairSemantics.raw2034step1 line 266
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2034 line 268
  62. def OAI.MUB6.Certificate.PairSemantics.raw2035 line 281
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2035 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw2036 line 287
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2036 line 289
  66. def OAI.MUB6.Certificate.PairSemantics.raw2037 line 293
  67. def OAI.MUB6.Certificate.PairSemantics.raw2037step0 line 295
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical2037 line 297
  69. def OAI.MUB6.Certificate.PairSemantics.raw2038 line 306
  70. def OAI.MUB6.Certificate.PairSemantics.raw2038step0 line 308
  71. def OAI.MUB6.Certificate.PairSemantics.raw2038step1 line 310
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2038 line 312
  73. def OAI.MUB6.Certificate.PairSemantics.raw2039 line 325
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2039 line 327
  75. def OAI.MUB6.Certificate.PairSemantics.raw2040 line 331
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2040 line 333
  77. def OAI.MUB6.Certificate.PairSemantics.raw2041 line 337
  78. def OAI.MUB6.Certificate.PairSemantics.raw2041step0 line 339
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2041 line 341
  80. def OAI.MUB6.Certificate.PairSemantics.raw2042 line 350
  81. def OAI.MUB6.Certificate.PairSemantics.raw2042step0 line 352
  82. def OAI.MUB6.Certificate.PairSemantics.raw2042step1 line 354
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2042 line 356
  84. def OAI.MUB6.Certificate.PairSemantics.raw2043 line 369
  85. def OAI.MUB6.Certificate.PairSemantics.raw2043step0 line 371
  86. def OAI.MUB6.Certificate.PairSemantics.raw2043step1 line 373
  87. def OAI.MUB6.Certificate.PairSemantics.raw2043step2 line 375
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2043 line 377
  89. def OAI.MUB6.Certificate.PairSemantics.raw2044 line 394
  90. def OAI.MUB6.Certificate.PairSemantics.raw2044step0 line 396
  91. def OAI.MUB6.Certificate.PairSemantics.raw2044step1 line 398
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2044 line 400
  93. def OAI.MUB6.Certificate.PairSemantics.raw2045 line 413
  94. def OAI.MUB6.Certificate.PairSemantics.raw2045step0 line 415
  95. def OAI.MUB6.Certificate.PairSemantics.raw2045step1 line 417
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical2045 line 419
  97. def OAI.MUB6.Certificate.PairSemantics.raw2046 line 432
  98. def OAI.MUB6.Certificate.PairSemantics.raw2046step0 line 434
  99. def OAI.MUB6.Certificate.PairSemantics.raw2046step1 line 436
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical2046 line 438
  101. def OAI.MUB6.Certificate.PairSemantics.raw2047 line 451
  102. def OAI.MUB6.Certificate.PairSemantics.raw2047step0 line 453
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical2047 line 455