OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical273.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8736 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw8736step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8736 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw8737 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw8737step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8737 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw8738 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw8738step0 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8738 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw8739 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw8739step0 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8739 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw8740 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw8740step0 line 71
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8740 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw8741 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw8741step0 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw8741step1 line 86
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8741 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw8742 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw8742step0 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw8742step1 line 105
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical8742 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw8743 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw8743step0 line 122
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical8743 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw8744 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw8744step0 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw8744step1 line 137
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical8744 line 139
  31. def OAI.MUB6.Certificate.PairSemantics.raw8745 line 153
  32. def OAI.MUB6.Certificate.PairSemantics.raw8745step0 line 155
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8745 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw8746 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw8746step0 line 168
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical8746 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw8747 line 179
  38. def OAI.MUB6.Certificate.PairSemantics.raw8747step0 line 181
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8747 line 183
  40. def OAI.MUB6.Certificate.PairSemantics.raw8748 line 192
  41. def OAI.MUB6.Certificate.PairSemantics.raw8748step0 line 194
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8748 line 196
  43. def OAI.MUB6.Certificate.PairSemantics.raw8749 line 205
  44. def OAI.MUB6.Certificate.PairSemantics.raw8749step0 line 207
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8749 line 209
  46. def OAI.MUB6.Certificate.PairSemantics.raw8750 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw8750step0 line 220
  48. def OAI.MUB6.Certificate.PairSemantics.raw8750step1 line 222
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8750 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw8751 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw8751step0 line 239
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical8751 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw8752 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw8752step0 line 252
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8752 line 254
  56. def OAI.MUB6.Certificate.PairSemantics.raw8753 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw8753step0 line 265
  58. def OAI.MUB6.Certificate.PairSemantics.raw8753step1 line 267
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8753 line 269
  60. def OAI.MUB6.Certificate.PairSemantics.raw8754 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw8754step0 line 284
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8754 line 286
  63. def OAI.MUB6.Certificate.PairSemantics.raw8755 line 295
  64. def OAI.MUB6.Certificate.PairSemantics.raw8755step0 line 297
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8755 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw8756 line 308
  67. def OAI.MUB6.Certificate.PairSemantics.raw8756step0 line 310
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8756 line 312
  69. def OAI.MUB6.Certificate.PairSemantics.raw8757 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw8757step0 line 323
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8757 line 325
  72. def OAI.MUB6.Certificate.PairSemantics.raw8758 line 334
  73. def OAI.MUB6.Certificate.PairSemantics.raw8758step0 line 336
  74. def OAI.MUB6.Certificate.PairSemantics.raw8758step1 line 338
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8758 line 340
  76. def OAI.MUB6.Certificate.PairSemantics.raw8759 line 353
  77. def OAI.MUB6.Certificate.PairSemantics.raw8759step0 line 355
  78. def OAI.MUB6.Certificate.PairSemantics.raw8759step1 line 357
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8759 line 359
  80. def OAI.MUB6.Certificate.PairSemantics.raw8760 line 372
  81. def OAI.MUB6.Certificate.PairSemantics.raw8760step0 line 374
  82. def OAI.MUB6.Certificate.PairSemantics.raw8760step1 line 376
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8760 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw8761 line 391
  85. def OAI.MUB6.Certificate.PairSemantics.raw8761step0 line 393
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8761 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw8762 line 404
  88. def OAI.MUB6.Certificate.PairSemantics.raw8762step0 line 406
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8762 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw8763 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw8763step0 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw8763step1 line 421
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8763 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw8764 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw8764step0 line 438
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8764 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw8765 line 449
  98. def OAI.MUB6.Certificate.PairSemantics.raw8765step0 line 451
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8765 line 453
  100. def OAI.MUB6.Certificate.PairSemantics.raw8766 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw8766step0 line 464
  102. def OAI.MUB6.Certificate.PairSemantics.raw8766step1 line 466
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical8766 line 468
  104. def OAI.MUB6.Certificate.PairSemantics.raw8767 line 481
  105. def OAI.MUB6.Certificate.PairSemantics.raw8767step0 line 483
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8767 line 485