OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical212.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6784 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw6784step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6784 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw6785 line 33
  5. def OAI.MUB6.Certificate.PairSemantics.raw6785step0 line 35
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6785 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw6786 line 46
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6786 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw6787 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw6787step0 line 54
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6787 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw6788 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6788 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw6789 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw6789step0 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw6789step1 line 76
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6789 line 78
  18. def OAI.MUB6.Certificate.PairSemantics.raw6790 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw6790step0 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw6790step1 line 95
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6790 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw6791 line 110
  23. def OAI.MUB6.Certificate.PairSemantics.raw6791step0 line 112
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6791 line 114
  25. def OAI.MUB6.Certificate.PairSemantics.raw6792 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw6792step0 line 125
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6792 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw6793 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw6793step0 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw6793step1 line 140
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6793 line 142
  32. def OAI.MUB6.Certificate.PairSemantics.raw6794 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw6794step0 line 157
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6794 line 159
  35. def OAI.MUB6.Certificate.PairSemantics.raw6795 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw6795step0 line 170
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6795 line 172
  38. def OAI.MUB6.Certificate.PairSemantics.raw6796 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw6796step0 line 183
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6796 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw6797 line 194
  42. def OAI.MUB6.Certificate.PairSemantics.raw6797step0 line 196
  43. def OAI.MUB6.Certificate.PairSemantics.raw6797step1 line 198
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6797 line 200
  45. def OAI.MUB6.Certificate.PairSemantics.raw6798 line 213
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6798 line 215
  47. def OAI.MUB6.Certificate.PairSemantics.raw6799 line 219
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6799 line 221
  49. def OAI.MUB6.Certificate.PairSemantics.raw6800 line 225
  50. def OAI.MUB6.Certificate.PairSemantics.raw6800step0 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw6800step1 line 229
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6800 line 231
  53. def OAI.MUB6.Certificate.PairSemantics.raw6801 line 244
  54. def OAI.MUB6.Certificate.PairSemantics.raw6801step0 line 246
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6801 line 248
  56. def OAI.MUB6.Certificate.PairSemantics.raw6802 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw6802step0 line 259
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6802 line 261
  59. def OAI.MUB6.Certificate.PairSemantics.raw6803 line 270
  60. def OAI.MUB6.Certificate.PairSemantics.raw6803step0 line 272
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical6803 line 274
  62. def OAI.MUB6.Certificate.PairSemantics.raw6804 line 283
  63. def OAI.MUB6.Certificate.PairSemantics.raw6804step0 line 285
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6804 line 287
  65. def OAI.MUB6.Certificate.PairSemantics.raw6805 line 297
  66. def OAI.MUB6.Certificate.PairSemantics.raw6805step0 line 299
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6805 line 301
  68. def OAI.MUB6.Certificate.PairSemantics.raw6806 line 311
  69. def OAI.MUB6.Certificate.PairSemantics.raw6806step0 line 313
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6806 line 315
  71. def OAI.MUB6.Certificate.PairSemantics.raw6807 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6807 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw6808 line 331
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6808 line 333
  75. def OAI.MUB6.Certificate.PairSemantics.raw6809 line 337
  76. def OAI.MUB6.Certificate.PairSemantics.raw6809step0 line 339
  77. def OAI.MUB6.Certificate.PairSemantics.raw6809step1 line 341
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6809 line 343
  79. def OAI.MUB6.Certificate.PairSemantics.raw6810 line 356
  80. def OAI.MUB6.Certificate.PairSemantics.raw6810step0 line 358
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6810 line 360
  82. def OAI.MUB6.Certificate.PairSemantics.raw6811 line 369
  83. def OAI.MUB6.Certificate.PairSemantics.raw6811step0 line 371
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6811 line 373
  85. def OAI.MUB6.Certificate.PairSemantics.raw6812 line 382
  86. def OAI.MUB6.Certificate.PairSemantics.raw6812step0 line 384
  87. def OAI.MUB6.Certificate.PairSemantics.raw6812step1 line 386
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6812 line 388
  89. def OAI.MUB6.Certificate.PairSemantics.raw6813 line 401
  90. def OAI.MUB6.Certificate.PairSemantics.raw6813step0 line 403
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6813 line 405
  92. def OAI.MUB6.Certificate.PairSemantics.raw6814 line 414
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6814 line 416
  94. def OAI.MUB6.Certificate.PairSemantics.raw6815 line 420
  95. def OAI.MUB6.Certificate.PairSemantics.raw6815step0 line 422
  96. def OAI.MUB6.Certificate.PairSemantics.raw6815step1 line 424
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6815 line 426