OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical73.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2336 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw2336step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2336 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw2337 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw2337step0 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw2337step1 line 31
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2337 line 33
  8. def OAI.MUB6.Certificate.PairSemantics.raw2338 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2338 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw2339 line 52
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2339 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw2340 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2340 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw2341 line 64
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2341 line 66
  16. def OAI.MUB6.Certificate.PairSemantics.raw2342 line 70
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2342 line 72
  18. def OAI.MUB6.Certificate.PairSemantics.raw2343 line 76
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2343 line 78
  20. def OAI.MUB6.Certificate.PairSemantics.raw2344 line 82
  21. def OAI.MUB6.Certificate.PairSemantics.raw2344step0 line 84
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2344 line 86
  23. def OAI.MUB6.Certificate.PairSemantics.raw2345 line 95
  24. def OAI.MUB6.Certificate.PairSemantics.raw2345step0 line 97
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2345 line 99
  26. def OAI.MUB6.Certificate.PairSemantics.raw2346 line 108
  27. def OAI.MUB6.Certificate.PairSemantics.raw2346step0 line 110
  28. def OAI.MUB6.Certificate.PairSemantics.raw2346step1 line 112
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical2346 line 114
  30. def OAI.MUB6.Certificate.PairSemantics.raw2347 line 127
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2347 line 129
  32. def OAI.MUB6.Certificate.PairSemantics.raw2348 line 133
  33. def OAI.MUB6.Certificate.PairSemantics.raw2348step0 line 135
  34. def OAI.MUB6.Certificate.PairSemantics.raw2348step1 line 137
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical2348 line 139
  36. def OAI.MUB6.Certificate.PairSemantics.raw2349 line 152
  37. def OAI.MUB6.Certificate.PairSemantics.raw2349step0 line 154
  38. def OAI.MUB6.Certificate.PairSemantics.raw2349step1 line 156
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2349 line 158
  40. def OAI.MUB6.Certificate.PairSemantics.raw2350 line 171
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical2350 line 173
  42. def OAI.MUB6.Certificate.PairSemantics.raw2351 line 177
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2351 line 179
  44. def OAI.MUB6.Certificate.PairSemantics.raw2352 line 183
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2352 line 185
  46. def OAI.MUB6.Certificate.PairSemantics.raw2353 line 189
  47. def OAI.MUB6.Certificate.PairSemantics.raw2353step0 line 191
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2353 line 193
  49. def OAI.MUB6.Certificate.PairSemantics.raw2354 line 202
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical2354 line 204
  51. def OAI.MUB6.Certificate.PairSemantics.raw2355 line 208
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2355 line 210
  53. def OAI.MUB6.Certificate.PairSemantics.raw2356 line 214
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2356 line 216
  55. def OAI.MUB6.Certificate.PairSemantics.raw2357 line 220
  56. def OAI.MUB6.Certificate.PairSemantics.raw2357step0 line 222
  57. def OAI.MUB6.Certificate.PairSemantics.raw2357step1 line 224
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical2357 line 226
  59. def OAI.MUB6.Certificate.PairSemantics.raw2358 line 239
  60. def OAI.MUB6.Certificate.PairSemantics.raw2358step0 line 241
  61. def OAI.MUB6.Certificate.PairSemantics.raw2358step1 line 243
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2358 line 245
  63. def OAI.MUB6.Certificate.PairSemantics.raw2359 line 258
  64. def OAI.MUB6.Certificate.PairSemantics.raw2359step0 line 260
  65. def OAI.MUB6.Certificate.PairSemantics.raw2359step1 line 262
  66. def OAI.MUB6.Certificate.PairSemantics.raw2359step2 line 264
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2359 line 266
  68. def OAI.MUB6.Certificate.PairSemantics.raw2360 line 283
  69. def OAI.MUB6.Certificate.PairSemantics.raw2360step0 line 285
  70. def OAI.MUB6.Certificate.PairSemantics.raw2360step1 line 287
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2360 line 289
  72. def OAI.MUB6.Certificate.PairSemantics.raw2361 line 302
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical2361 line 304
  74. def OAI.MUB6.Certificate.PairSemantics.raw2362 line 308
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2362 line 310
  76. def OAI.MUB6.Certificate.PairSemantics.raw2363 line 314
  77. def OAI.MUB6.Certificate.PairSemantics.raw2363step0 line 316
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2363 line 318
  79. def OAI.MUB6.Certificate.PairSemantics.raw2364 line 327
  80. def OAI.MUB6.Certificate.PairSemantics.raw2364step0 line 329
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical2364 line 331
  82. def OAI.MUB6.Certificate.PairSemantics.raw2365 line 340
  83. def OAI.MUB6.Certificate.PairSemantics.raw2365step0 line 342
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2365 line 344
  85. def OAI.MUB6.Certificate.PairSemantics.raw2366 line 353
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2366 line 355
  87. def OAI.MUB6.Certificate.PairSemantics.raw2367 line 359
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2367 line 361