OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical213.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6816 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw6816step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6816 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw6817 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw6817step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6817 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw6818 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6818 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw6819 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw6819step0 line 51
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6819 line 53
  12. def OAI.MUB6.Certificate.PairSemantics.raw6820 line 62
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6820 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw6821 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw6821step0 line 70
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6821 line 72
  17. def OAI.MUB6.Certificate.PairSemantics.raw6822 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw6822step0 line 84
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6822 line 86
  20. def OAI.MUB6.Certificate.PairSemantics.raw6823 line 95
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6823 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw6824 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw6824step0 line 103
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6824 line 105
  25. def OAI.MUB6.Certificate.PairSemantics.raw6825 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw6825step0 line 116
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6825 line 118
  28. def OAI.MUB6.Certificate.PairSemantics.raw6826 line 127
  29. def OAI.MUB6.Certificate.PairSemantics.raw6826step0 line 129
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6826 line 131
  31. def OAI.MUB6.Certificate.PairSemantics.raw6827 line 140
  32. def OAI.MUB6.Certificate.PairSemantics.raw6827step0 line 142
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical6827 line 144
  34. def OAI.MUB6.Certificate.PairSemantics.raw6828 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw6828step0 line 155
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6828 line 157
  37. def OAI.MUB6.Certificate.PairSemantics.raw6829 line 166
  38. def OAI.MUB6.Certificate.PairSemantics.raw6829step0 line 168
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6829 line 170
  40. def OAI.MUB6.Certificate.PairSemantics.raw6830 line 180
  41. def OAI.MUB6.Certificate.PairSemantics.raw6830step0 line 182
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6830 line 184
  43. def OAI.MUB6.Certificate.PairSemantics.raw6831 line 194
  44. def OAI.MUB6.Certificate.PairSemantics.raw6831step0 line 196
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6831 line 198
  46. def OAI.MUB6.Certificate.PairSemantics.raw6832 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw6832step0 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw6832step1 line 212
  49. def OAI.MUB6.Certificate.PairSemantics.raw6832step2 line 214
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6832 line 216
  51. def OAI.MUB6.Certificate.PairSemantics.raw6833 line 234
  52. def OAI.MUB6.Certificate.PairSemantics.raw6833step0 line 236
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical6833 line 238
  54. def OAI.MUB6.Certificate.PairSemantics.raw6834 line 247
  55. def OAI.MUB6.Certificate.PairSemantics.raw6834step0 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw6834step1 line 251
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6834 line 253
  58. def OAI.MUB6.Certificate.PairSemantics.raw6835 line 266
  59. def OAI.MUB6.Certificate.PairSemantics.raw6835step0 line 268
  60. def OAI.MUB6.Certificate.PairSemantics.raw6835step1 line 270
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical6835 line 272
  62. def OAI.MUB6.Certificate.PairSemantics.raw6836 line 285
  63. def OAI.MUB6.Certificate.PairSemantics.raw6836step0 line 287
  64. def OAI.MUB6.Certificate.PairSemantics.raw6836step1 line 289
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6836 line 291
  66. def OAI.MUB6.Certificate.PairSemantics.raw6837 line 304
  67. def OAI.MUB6.Certificate.PairSemantics.raw6837step0 line 306
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6837 line 308
  69. def OAI.MUB6.Certificate.PairSemantics.raw6838 line 317
  70. def OAI.MUB6.Certificate.PairSemantics.raw6838step0 line 319
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6838 line 321
  72. def OAI.MUB6.Certificate.PairSemantics.raw6839 line 331
  73. def OAI.MUB6.Certificate.PairSemantics.raw6839step0 line 333
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6839 line 335
  75. def OAI.MUB6.Certificate.PairSemantics.raw6840 line 345
  76. def OAI.MUB6.Certificate.PairSemantics.raw6840step0 line 347
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6840 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw6841 line 358
  79. def OAI.MUB6.Certificate.PairSemantics.raw6841step0 line 360
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6841 line 362
  81. def OAI.MUB6.Certificate.PairSemantics.raw6842 line 371
  82. def OAI.MUB6.Certificate.PairSemantics.raw6842step0 line 373
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6842 line 375
  84. def OAI.MUB6.Certificate.PairSemantics.raw6843 line 385
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6843 line 387
  86. def OAI.MUB6.Certificate.PairSemantics.raw6844 line 391
  87. def OAI.MUB6.Certificate.PairSemantics.raw6844step0 line 393
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6844 line 395
  89. def OAI.MUB6.Certificate.PairSemantics.raw6845 line 404
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6845 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw6846 line 410
  92. def OAI.MUB6.Certificate.PairSemantics.raw6846step0 line 412
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6846 line 414
  94. def OAI.MUB6.Certificate.PairSemantics.raw6847 line 423
  95. def OAI.MUB6.Certificate.PairSemantics.raw6847step0 line 425
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical6847 line 427