OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical210.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6720 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw6720step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6720 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw6721 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw6721step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6721 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw6722 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw6722step0 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw6722step1 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6722 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw6723 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6723 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw6724 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw6724step0 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6724 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw6725 line 78
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6725 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw6726 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw6726step0 line 86
  20. def OAI.MUB6.Certificate.PairSemantics.raw6726step1 line 88
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6726 line 90
  22. def OAI.MUB6.Certificate.PairSemantics.raw6727 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw6727step0 line 105
  24. def OAI.MUB6.Certificate.PairSemantics.raw6727step1 line 107
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6727 line 109
  26. def OAI.MUB6.Certificate.PairSemantics.raw6728 line 122
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6728 line 124
  28. def OAI.MUB6.Certificate.PairSemantics.raw6729 line 128
  29. def OAI.MUB6.Certificate.PairSemantics.raw6729step0 line 130
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6729 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw6730 line 141
  32. def OAI.MUB6.Certificate.PairSemantics.raw6730step0 line 143
  33. def OAI.MUB6.Certificate.PairSemantics.raw6730step1 line 145
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6730 line 147
  35. def OAI.MUB6.Certificate.PairSemantics.raw6731 line 160
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6731 line 162
  37. def OAI.MUB6.Certificate.PairSemantics.raw6732 line 166
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6732 line 168
  39. def OAI.MUB6.Certificate.PairSemantics.raw6733 line 172
  40. def OAI.MUB6.Certificate.PairSemantics.raw6733step0 line 174
  41. def OAI.MUB6.Certificate.PairSemantics.raw6733step1 line 176
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6733 line 178
  43. def OAI.MUB6.Certificate.PairSemantics.raw6734 line 191
  44. def OAI.MUB6.Certificate.PairSemantics.raw6734step0 line 193
  45. def OAI.MUB6.Certificate.PairSemantics.raw6734step1 line 195
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6734 line 197
  47. def OAI.MUB6.Certificate.PairSemantics.raw6735 line 210
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6735 line 212
  49. def OAI.MUB6.Certificate.PairSemantics.raw6736 line 216
  50. def OAI.MUB6.Certificate.PairSemantics.raw6736step0 line 218
  51. def OAI.MUB6.Certificate.PairSemantics.raw6736step1 line 220
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6736 line 222
  53. def OAI.MUB6.Certificate.PairSemantics.raw6737 line 235
  54. def OAI.MUB6.Certificate.PairSemantics.raw6737step0 line 237
  55. def OAI.MUB6.Certificate.PairSemantics.raw6737step1 line 239
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6737 line 241
  57. def OAI.MUB6.Certificate.PairSemantics.raw6738 line 254
  58. def OAI.MUB6.Certificate.PairSemantics.raw6738step0 line 256
  59. def OAI.MUB6.Certificate.PairSemantics.raw6738step1 line 258
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6738 line 260
  61. def OAI.MUB6.Certificate.PairSemantics.raw6739 line 273
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6739 line 275
  63. def OAI.MUB6.Certificate.PairSemantics.raw6740 line 279
  64. def OAI.MUB6.Certificate.PairSemantics.raw6740step0 line 281
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6740 line 283
  66. def OAI.MUB6.Certificate.PairSemantics.raw6741 line 292
  67. def OAI.MUB6.Certificate.PairSemantics.raw6741step0 line 294
  68. def OAI.MUB6.Certificate.PairSemantics.raw6741step1 line 296
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6741 line 298
  70. def OAI.MUB6.Certificate.PairSemantics.raw6742 line 311
  71. def OAI.MUB6.Certificate.PairSemantics.raw6742step0 line 313
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6742 line 315
  73. def OAI.MUB6.Certificate.PairSemantics.raw6743 line 324
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6743 line 326
  75. def OAI.MUB6.Certificate.PairSemantics.raw6744 line 330
  76. def OAI.MUB6.Certificate.PairSemantics.raw6744step0 line 332
  77. def OAI.MUB6.Certificate.PairSemantics.raw6744step1 line 334
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6744 line 336
  79. def OAI.MUB6.Certificate.PairSemantics.raw6745 line 349
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6745 line 351
  81. def OAI.MUB6.Certificate.PairSemantics.raw6746 line 355
  82. def OAI.MUB6.Certificate.PairSemantics.raw6746step0 line 357
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6746 line 359
  84. def OAI.MUB6.Certificate.PairSemantics.raw6747 line 368
  85. def OAI.MUB6.Certificate.PairSemantics.raw6747step0 line 370
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6747 line 372
  87. def OAI.MUB6.Certificate.PairSemantics.raw6748 line 381
  88. def OAI.MUB6.Certificate.PairSemantics.raw6748step0 line 383
  89. def OAI.MUB6.Certificate.PairSemantics.raw6748step1 line 385
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6748 line 387
  91. def OAI.MUB6.Certificate.PairSemantics.raw6749 line 400
  92. def OAI.MUB6.Certificate.PairSemantics.raw6749step0 line 402
  93. def OAI.MUB6.Certificate.PairSemantics.raw6749step1 line 404
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical6749 line 406
  95. def OAI.MUB6.Certificate.PairSemantics.raw6750 line 419
  96. def OAI.MUB6.Certificate.PairSemantics.raw6750step0 line 421
  97. def OAI.MUB6.Certificate.PairSemantics.raw6750step1 line 423
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical6750 line 425
  99. def OAI.MUB6.Certificate.PairSemantics.raw6751 line 438
  100. def OAI.MUB6.Certificate.PairSemantics.raw6751step0 line 440
  101. def OAI.MUB6.Certificate.PairSemantics.raw6751step1 line 442
  102. def OAI.MUB6.Certificate.PairSemantics.raw6751step2 line 444
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6751 line 446