OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical129.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4128 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw4128step0 line 14
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical4128 line 16
  4. def OAI.MUB6.Certificate.PairSemantics.raw4129 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw4129step0 line 28
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical4129 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw4130 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4130 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw4131 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw4131step0 line 47
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4131 line 49
  12. def OAI.MUB6.Certificate.PairSemantics.raw4132 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw4132step0 line 60
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4132 line 62
  15. def OAI.MUB6.Certificate.PairSemantics.raw4133 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw4133step0 line 73
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4133 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw4134 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw4134step0 line 86
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4134 line 88
  21. def OAI.MUB6.Certificate.PairSemantics.raw4135 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw4135step0 line 99
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4135 line 101
  24. def OAI.MUB6.Certificate.PairSemantics.raw4136 line 110
  25. def OAI.MUB6.Certificate.PairSemantics.raw4136step0 line 112
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4136 line 114
  27. def OAI.MUB6.Certificate.PairSemantics.raw4137 line 123
  28. def OAI.MUB6.Certificate.PairSemantics.raw4137step0 line 125
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4137 line 127
  30. def OAI.MUB6.Certificate.PairSemantics.raw4138 line 136
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4138 line 138
  32. def OAI.MUB6.Certificate.PairSemantics.raw4139 line 142
  33. def OAI.MUB6.Certificate.PairSemantics.raw4139step0 line 144
  34. def OAI.MUB6.Certificate.PairSemantics.raw4139step1 line 146
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4139 line 148
  36. def OAI.MUB6.Certificate.PairSemantics.raw4140 line 161
  37. def OAI.MUB6.Certificate.PairSemantics.raw4140step0 line 163
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4140 line 165
  39. def OAI.MUB6.Certificate.PairSemantics.raw4141 line 174
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4141 line 176
  41. def OAI.MUB6.Certificate.PairSemantics.raw4142 line 180
  42. def OAI.MUB6.Certificate.PairSemantics.raw4142step0 line 182
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4142 line 184
  44. def OAI.MUB6.Certificate.PairSemantics.raw4143 line 193
  45. def OAI.MUB6.Certificate.PairSemantics.raw4143step0 line 195
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4143 line 197
  47. def OAI.MUB6.Certificate.PairSemantics.raw4144 line 206
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4144 line 208
  49. def OAI.MUB6.Certificate.PairSemantics.raw4145 line 212
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4145 line 214
  51. def OAI.MUB6.Certificate.PairSemantics.raw4146 line 218
  52. def OAI.MUB6.Certificate.PairSemantics.raw4146step0 line 220
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4146 line 222
  54. def OAI.MUB6.Certificate.PairSemantics.raw4147 line 231
  55. def OAI.MUB6.Certificate.PairSemantics.raw4147step0 line 233
  56. def OAI.MUB6.Certificate.PairSemantics.raw4147step1 line 235
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4147 line 237
  58. def OAI.MUB6.Certificate.PairSemantics.raw4148 line 250
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4148 line 252
  60. def OAI.MUB6.Certificate.PairSemantics.raw4149 line 256
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4149 line 258
  62. def OAI.MUB6.Certificate.PairSemantics.raw4150 line 262
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical4150 line 264
  64. def OAI.MUB6.Certificate.PairSemantics.raw4151 line 268
  65. def OAI.MUB6.Certificate.PairSemantics.raw4151step0 line 270
  66. def OAI.MUB6.Certificate.PairSemantics.raw4151step1 line 272
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4151 line 274
  68. def OAI.MUB6.Certificate.PairSemantics.raw4152 line 287
  69. def OAI.MUB6.Certificate.PairSemantics.raw4152step0 line 289
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4152 line 291
  71. def OAI.MUB6.Certificate.PairSemantics.raw4153 line 300
  72. def OAI.MUB6.Certificate.PairSemantics.raw4153step0 line 302
  73. def OAI.MUB6.Certificate.PairSemantics.raw4153step1 line 304
  74. def OAI.MUB6.Certificate.PairSemantics.raw4153step2 line 306
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4153 line 308
  76. def OAI.MUB6.Certificate.PairSemantics.raw4154 line 325
  77. def OAI.MUB6.Certificate.PairSemantics.raw4154step0 line 327
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical4154 line 329
  79. def OAI.MUB6.Certificate.PairSemantics.raw4155 line 338
  80. def OAI.MUB6.Certificate.PairSemantics.raw4155step0 line 340
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4155 line 342
  82. def OAI.MUB6.Certificate.PairSemantics.raw4156 line 351
  83. def OAI.MUB6.Certificate.PairSemantics.raw4156step0 line 353
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4156 line 355
  85. def OAI.MUB6.Certificate.PairSemantics.raw4157 line 364
  86. def OAI.MUB6.Certificate.PairSemantics.raw4157step0 line 366
  87. def OAI.MUB6.Certificate.PairSemantics.raw4157step1 line 368
  88. def OAI.MUB6.Certificate.PairSemantics.raw4157step2 line 370
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4157 line 372
  90. def OAI.MUB6.Certificate.PairSemantics.raw4158 line 389
  91. def OAI.MUB6.Certificate.PairSemantics.raw4158step0 line 391
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical4158 line 393
  93. def OAI.MUB6.Certificate.PairSemantics.raw4159 line 402
  94. def OAI.MUB6.Certificate.PairSemantics.raw4159step0 line 404
  95. def OAI.MUB6.Certificate.PairSemantics.raw4159step1 line 406
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4159 line 408