OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical301.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9632 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw9632step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9632 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw9633 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw9633step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9633 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw9634 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw9634step0 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9634 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw9635 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw9635step0 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9635 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw9636 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw9636step0 line 71
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9636 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw9637 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw9637step0 line 84
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9637 line 86
  19. def OAI.MUB6.Certificate.PairSemantics.raw9638 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw9638step0 line 97
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9638 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw9639 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw9639step0 line 110
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9639 line 112
  25. def OAI.MUB6.Certificate.PairSemantics.raw9640 line 121
  26. def OAI.MUB6.Certificate.PairSemantics.raw9640step0 line 123
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9640 line 125
  28. def OAI.MUB6.Certificate.PairSemantics.raw9641 line 134
  29. def OAI.MUB6.Certificate.PairSemantics.raw9641step0 line 136
  30. def OAI.MUB6.Certificate.PairSemantics.raw9641step1 line 138
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9641 line 140
  32. def OAI.MUB6.Certificate.PairSemantics.raw9642 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw9642step0 line 155
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9642 line 157
  35. def OAI.MUB6.Certificate.PairSemantics.raw9643 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw9643step0 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9643 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw9644 line 179
  39. def OAI.MUB6.Certificate.PairSemantics.raw9644step0 line 181
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9644 line 183
  41. def OAI.MUB6.Certificate.PairSemantics.raw9645 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw9645step0 line 194
  43. def OAI.MUB6.Certificate.PairSemantics.raw9645step1 line 196
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9645 line 198
  45. def OAI.MUB6.Certificate.PairSemantics.raw9646 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw9646step0 line 213
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9646 line 215
  48. def OAI.MUB6.Certificate.PairSemantics.raw9647 line 224
  49. def OAI.MUB6.Certificate.PairSemantics.raw9647step0 line 226
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9647 line 228
  51. def OAI.MUB6.Certificate.PairSemantics.raw9648 line 237
  52. def OAI.MUB6.Certificate.PairSemantics.raw9648step0 line 239
  53. def OAI.MUB6.Certificate.PairSemantics.raw9648step1 line 241
  54. def OAI.MUB6.Certificate.PairSemantics.raw9648step2 line 243
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9648 line 245
  56. def OAI.MUB6.Certificate.PairSemantics.raw9649 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw9649step0 line 265
  58. def OAI.MUB6.Certificate.PairSemantics.raw9649step1 line 267
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9649 line 269
  60. def OAI.MUB6.Certificate.PairSemantics.raw9650 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw9650step0 line 284
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9650 line 286
  63. def OAI.MUB6.Certificate.PairSemantics.raw9651 line 295
  64. def OAI.MUB6.Certificate.PairSemantics.raw9651step0 line 297
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9651 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw9652 line 308
  67. def OAI.MUB6.Certificate.PairSemantics.raw9652step0 line 310
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9652 line 312
  69. def OAI.MUB6.Certificate.PairSemantics.raw9653 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw9653step0 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw9653step1 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9653 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw9654 line 340
  74. def OAI.MUB6.Certificate.PairSemantics.raw9654step0 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw9654step1 line 344
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical9654 line 346
  77. def OAI.MUB6.Certificate.PairSemantics.raw9655 line 359
  78. def OAI.MUB6.Certificate.PairSemantics.raw9655step0 line 361
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical9655 line 363
  80. def OAI.MUB6.Certificate.PairSemantics.raw9656 line 372
  81. def OAI.MUB6.Certificate.PairSemantics.raw9656step0 line 374
  82. def OAI.MUB6.Certificate.PairSemantics.raw9656step1 line 376
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9656 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw9657 line 391
  85. def OAI.MUB6.Certificate.PairSemantics.raw9657step0 line 393
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9657 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw9658 line 404
  88. def OAI.MUB6.Certificate.PairSemantics.raw9658step0 line 406
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9658 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw9659 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw9659step0 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw9659step1 line 421
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9659 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw9660 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw9660step0 line 438
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9660 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw9661 line 449
  98. def OAI.MUB6.Certificate.PairSemantics.raw9661step0 line 451
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9661 line 453
  100. def OAI.MUB6.Certificate.PairSemantics.raw9662 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw9662step0 line 464
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9662 line 466
  103. def OAI.MUB6.Certificate.PairSemantics.raw9663 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw9663step0 line 477
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical9663 line 479