OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical195.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6240 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw6240step0 line 15
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6240 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw6241 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6241 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw6242 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw6242step0 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6242 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw6243 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw6243step0 line 47
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6243 line 49
  12. def OAI.MUB6.Certificate.PairSemantics.raw6244 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw6244step0 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw6244step1 line 62
  15. def OAI.MUB6.Certificate.PairSemantics.raw6244step2 line 64
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6244 line 66
  17. def OAI.MUB6.Certificate.PairSemantics.raw6245 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw6245step0 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw6245step1 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw6245step2 line 89
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6245 line 91
  22. def OAI.MUB6.Certificate.PairSemantics.raw6246 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw6246step0 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw6246step1 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw6246step2 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6246 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw6247 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw6247step0 line 137
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6247 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw6248 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw6248step0 line 150
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6248 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw6249 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw6249step0 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw6249step1 line 165
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6249 line 167
  37. def OAI.MUB6.Certificate.PairSemantics.raw6250 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw6250step0 line 182
  39. def OAI.MUB6.Certificate.PairSemantics.raw6250step1 line 184
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6250 line 186
  41. def OAI.MUB6.Certificate.PairSemantics.raw6251 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw6251step0 line 201
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6251 line 203
  44. def OAI.MUB6.Certificate.PairSemantics.raw6252 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw6252step0 line 214
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6252 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw6253 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw6253step0 line 227
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6253 line 229
  50. def OAI.MUB6.Certificate.PairSemantics.raw6254 line 238
  51. def OAI.MUB6.Certificate.PairSemantics.raw6254step0 line 240
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6254 line 242
  53. def OAI.MUB6.Certificate.PairSemantics.raw6255 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw6255step0 line 254
  55. def OAI.MUB6.Certificate.PairSemantics.raw6255step1 line 256
  56. def OAI.MUB6.Certificate.PairSemantics.raw6255step2 line 258
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6255 line 260
  58. def OAI.MUB6.Certificate.PairSemantics.raw6256 line 278
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6256 line 280
  60. def OAI.MUB6.Certificate.PairSemantics.raw6257 line 284
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical6257 line 286
  62. def OAI.MUB6.Certificate.PairSemantics.raw6258 line 290
  63. def OAI.MUB6.Certificate.PairSemantics.raw6258step0 line 292
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6258 line 294
  65. def OAI.MUB6.Certificate.PairSemantics.raw6259 line 303
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6259 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw6260 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw6260step0 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6260 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw6261 line 322
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6261 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw6262 line 328
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6262 line 330
  74. def OAI.MUB6.Certificate.PairSemantics.raw6263 line 334
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6263 line 336
  76. def OAI.MUB6.Certificate.PairSemantics.raw6264 line 340
  77. def OAI.MUB6.Certificate.PairSemantics.raw6264step0 line 342
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6264 line 344
  79. def OAI.MUB6.Certificate.PairSemantics.raw6265 line 353
  80. def OAI.MUB6.Certificate.PairSemantics.raw6265step0 line 355
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6265 line 357
  82. def OAI.MUB6.Certificate.PairSemantics.raw6266 line 366
  83. def OAI.MUB6.Certificate.PairSemantics.raw6266step0 line 368
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6266 line 370
  85. def OAI.MUB6.Certificate.PairSemantics.raw6267 line 379
  86. def OAI.MUB6.Certificate.PairSemantics.raw6267step0 line 381
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical6267 line 383
  88. def OAI.MUB6.Certificate.PairSemantics.raw6268 line 392
  89. def OAI.MUB6.Certificate.PairSemantics.raw6268step0 line 394
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6268 line 396
  91. def OAI.MUB6.Certificate.PairSemantics.raw6269 line 405
  92. def OAI.MUB6.Certificate.PairSemantics.raw6269step0 line 407
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6269 line 409
  94. def OAI.MUB6.Certificate.PairSemantics.raw6270 line 418
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6270 line 420
  96. def OAI.MUB6.Certificate.PairSemantics.raw6271 line 424
  97. def OAI.MUB6.Certificate.PairSemantics.raw6271step0 line 426
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical6271 line 428