OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical296.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9472 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw9472step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9472 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw9473 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw9473step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9473 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw9474 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw9474step0 line 42
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9474 line 44
  10. def OAI.MUB6.Certificate.PairSemantics.raw9475 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw9475step0 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9475 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw9476 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw9476step0 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9476 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw9477 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw9477step0 line 81
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9477 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw9478 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw9478step0 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw9478step1 line 96
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9478 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw9479 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw9479step0 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw9479step1 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9479 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw9480 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw9480step0 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw9480step1 line 134
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9480 line 136
  31. def OAI.MUB6.Certificate.PairSemantics.raw9481 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw9481step0 line 151
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9481 line 153
  34. def OAI.MUB6.Certificate.PairSemantics.raw9482 line 162
  35. def OAI.MUB6.Certificate.PairSemantics.raw9482step0 line 164
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9482 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw9483 line 175
  38. def OAI.MUB6.Certificate.PairSemantics.raw9483step0 line 177
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9483 line 179
  40. def OAI.MUB6.Certificate.PairSemantics.raw9484 line 188
  41. def OAI.MUB6.Certificate.PairSemantics.raw9484step0 line 190
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9484 line 192
  43. def OAI.MUB6.Certificate.PairSemantics.raw9485 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw9485step0 line 203
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9485 line 205
  46. def OAI.MUB6.Certificate.PairSemantics.raw9486 line 214
  47. def OAI.MUB6.Certificate.PairSemantics.raw9486step0 line 216
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9486 line 218
  49. def OAI.MUB6.Certificate.PairSemantics.raw9487 line 227
  50. def OAI.MUB6.Certificate.PairSemantics.raw9487step0 line 229
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical9487 line 231
  52. def OAI.MUB6.Certificate.PairSemantics.raw9488 line 240
  53. def OAI.MUB6.Certificate.PairSemantics.raw9488step0 line 242
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9488 line 244
  55. def OAI.MUB6.Certificate.PairSemantics.raw9489 line 253
  56. def OAI.MUB6.Certificate.PairSemantics.raw9489step0 line 255
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9489 line 257
  58. def OAI.MUB6.Certificate.PairSemantics.raw9490 line 266
  59. def OAI.MUB6.Certificate.PairSemantics.raw9490step0 line 268
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical9490 line 270
  61. def OAI.MUB6.Certificate.PairSemantics.raw9491 line 279
  62. def OAI.MUB6.Certificate.PairSemantics.raw9491step0 line 281
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9491 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw9492 line 292
  65. def OAI.MUB6.Certificate.PairSemantics.raw9492step0 line 294
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9492 line 296
  67. def OAI.MUB6.Certificate.PairSemantics.raw9493 line 305
  68. def OAI.MUB6.Certificate.PairSemantics.raw9493step0 line 307
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9493 line 309
  70. def OAI.MUB6.Certificate.PairSemantics.raw9494 line 318
  71. def OAI.MUB6.Certificate.PairSemantics.raw9494step0 line 320
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9494 line 322
  73. def OAI.MUB6.Certificate.PairSemantics.raw9495 line 331
  74. def OAI.MUB6.Certificate.PairSemantics.raw9495step0 line 333
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9495 line 335
  76. def OAI.MUB6.Certificate.PairSemantics.raw9496 line 344
  77. def OAI.MUB6.Certificate.PairSemantics.raw9496step0 line 346
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9496 line 348
  79. def OAI.MUB6.Certificate.PairSemantics.raw9497 line 357
  80. def OAI.MUB6.Certificate.PairSemantics.raw9497step0 line 359
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9497 line 361
  82. def OAI.MUB6.Certificate.PairSemantics.raw9498 line 370
  83. def OAI.MUB6.Certificate.PairSemantics.raw9498step0 line 372
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9498 line 374
  85. def OAI.MUB6.Certificate.PairSemantics.raw9499 line 383
  86. def OAI.MUB6.Certificate.PairSemantics.raw9499step0 line 385
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9499 line 387
  88. def OAI.MUB6.Certificate.PairSemantics.raw9500 line 396
  89. def OAI.MUB6.Certificate.PairSemantics.raw9500step0 line 398
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical9500 line 400
  91. def OAI.MUB6.Certificate.PairSemantics.raw9501 line 409
  92. def OAI.MUB6.Certificate.PairSemantics.raw9501step0 line 411
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9501 line 413
  94. def OAI.MUB6.Certificate.PairSemantics.raw9502 line 422
  95. def OAI.MUB6.Certificate.PairSemantics.raw9502step0 line 424
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9502 line 426
  97. def OAI.MUB6.Certificate.PairSemantics.raw9503 line 435
  98. def OAI.MUB6.Certificate.PairSemantics.raw9503step0 line 437
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9503 line 439