OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical188.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6016 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw6016step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6016 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw6017 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw6017step0 line 33
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6017 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw6018 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6018 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw6019 line 50
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6019 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw6020 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw6020step0 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6020 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw6021 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6021 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw6022 line 75
  17. def OAI.MUB6.Certificate.PairSemantics.raw6022step0 line 77
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6022 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw6023 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw6023step0 line 90
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6023 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw6024 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw6024step0 line 103
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6024 line 105
  25. def OAI.MUB6.Certificate.PairSemantics.raw6025 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw6025step0 line 116
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6025 line 118
  28. def OAI.MUB6.Certificate.PairSemantics.raw6026 line 127
  29. def OAI.MUB6.Certificate.PairSemantics.raw6026step0 line 129
  30. def OAI.MUB6.Certificate.PairSemantics.raw6026step1 line 131
  31. def OAI.MUB6.Certificate.PairSemantics.raw6026step2 line 133
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6026 line 135
  33. def OAI.MUB6.Certificate.PairSemantics.raw6027 line 152
  34. def OAI.MUB6.Certificate.PairSemantics.raw6027step0 line 154
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6027 line 156
  36. def OAI.MUB6.Certificate.PairSemantics.raw6028 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw6028step0 line 167
  38. def OAI.MUB6.Certificate.PairSemantics.raw6028step1 line 169
  39. def OAI.MUB6.Certificate.PairSemantics.raw6028step2 line 171
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6028 line 173
  41. def OAI.MUB6.Certificate.PairSemantics.raw6029 line 190
  42. def OAI.MUB6.Certificate.PairSemantics.raw6029step0 line 192
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6029 line 194
  44. def OAI.MUB6.Certificate.PairSemantics.raw6030 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw6030step0 line 205
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6030 line 207
  47. def OAI.MUB6.Certificate.PairSemantics.raw6031 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw6031step0 line 218
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6031 line 220
  50. def OAI.MUB6.Certificate.PairSemantics.raw6032 line 229
  51. def OAI.MUB6.Certificate.PairSemantics.raw6032step0 line 231
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6032 line 233
  53. def OAI.MUB6.Certificate.PairSemantics.raw6033 line 242
  54. def OAI.MUB6.Certificate.PairSemantics.raw6033step0 line 244
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6033 line 246
  56. def OAI.MUB6.Certificate.PairSemantics.raw6034 line 255
  57. def OAI.MUB6.Certificate.PairSemantics.raw6034step0 line 257
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6034 line 259
  59. def OAI.MUB6.Certificate.PairSemantics.raw6035 line 268
  60. def OAI.MUB6.Certificate.PairSemantics.raw6035step0 line 270
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical6035 line 272
  62. def OAI.MUB6.Certificate.PairSemantics.raw6036 line 281
  63. def OAI.MUB6.Certificate.PairSemantics.raw6036step0 line 283
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6036 line 285
  65. def OAI.MUB6.Certificate.PairSemantics.raw6037 line 294
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6037 line 296
  67. def OAI.MUB6.Certificate.PairSemantics.raw6038 line 300
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6038 line 302
  69. def OAI.MUB6.Certificate.PairSemantics.raw6039 line 306
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6039 line 308
  71. def OAI.MUB6.Certificate.PairSemantics.raw6040 line 312
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6040 line 314
  73. def OAI.MUB6.Certificate.PairSemantics.raw6041 line 318
  74. def OAI.MUB6.Certificate.PairSemantics.raw6041step0 line 320
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6041 line 322
  76. def OAI.MUB6.Certificate.PairSemantics.raw6042 line 331
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6042 line 333
  78. def OAI.MUB6.Certificate.PairSemantics.raw6043 line 337
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6043 line 339
  80. def OAI.MUB6.Certificate.PairSemantics.raw6044 line 343
  81. def OAI.MUB6.Certificate.PairSemantics.raw6044step0 line 345
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6044 line 347
  83. def OAI.MUB6.Certificate.PairSemantics.raw6045 line 356
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6045 line 358
  85. def OAI.MUB6.Certificate.PairSemantics.raw6046 line 362
  86. def OAI.MUB6.Certificate.PairSemantics.raw6046step0 line 364
  87. def OAI.MUB6.Certificate.PairSemantics.raw6046step1 line 366
  88. def OAI.MUB6.Certificate.PairSemantics.raw6046step2 line 368
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6046 line 370
  90. def OAI.MUB6.Certificate.PairSemantics.raw6047 line 387
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6047 line 389