OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical308.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9856 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw9856step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw9856step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9856 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw9857 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw9857step0 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw9857step1 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9857 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw9858 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw9858step0 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw9858step1 line 60
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9858 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw9859 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw9859step0 line 77
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9859 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw9860 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw9860step0 line 90
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9860 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw9861 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw9861step0 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw9861step1 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9861 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw9862 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw9862step0 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9862 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw9863 line 133
  27. def OAI.MUB6.Certificate.PairSemantics.raw9863step0 line 135
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9863 line 137
  29. def OAI.MUB6.Certificate.PairSemantics.raw9864 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw9864step0 line 148
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9864 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw9865 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw9865step0 line 161
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9865 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw9866 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw9866step0 line 174
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9866 line 176
  38. def OAI.MUB6.Certificate.PairSemantics.raw9867 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw9867step0 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9867 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw9868 line 198
  42. def OAI.MUB6.Certificate.PairSemantics.raw9868step0 line 200
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9868 line 202
  44. def OAI.MUB6.Certificate.PairSemantics.raw9869 line 211
  45. def OAI.MUB6.Certificate.PairSemantics.raw9869step0 line 213
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9869 line 215
  47. def OAI.MUB6.Certificate.PairSemantics.raw9870 line 224
  48. def OAI.MUB6.Certificate.PairSemantics.raw9870step0 line 226
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical9870 line 228
  50. def OAI.MUB6.Certificate.PairSemantics.raw9871 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw9871step0 line 239
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9871 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw9872 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw9872step0 line 252
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9872 line 254
  56. def OAI.MUB6.Certificate.PairSemantics.raw9873 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw9873step0 line 265
  58. def OAI.MUB6.Certificate.PairSemantics.raw9873step1 line 267
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9873 line 269
  60. def OAI.MUB6.Certificate.PairSemantics.raw9874 line 283
  61. def OAI.MUB6.Certificate.PairSemantics.raw9874step0 line 285
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9874 line 287
  63. def OAI.MUB6.Certificate.PairSemantics.raw9875 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw9875step0 line 298
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9875 line 300
  66. def OAI.MUB6.Certificate.PairSemantics.raw9876 line 309
  67. def OAI.MUB6.Certificate.PairSemantics.raw9876step0 line 311
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9876 line 313
  69. def OAI.MUB6.Certificate.PairSemantics.raw9877 line 322
  70. def OAI.MUB6.Certificate.PairSemantics.raw9877step0 line 324
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9877 line 326
  72. def OAI.MUB6.Certificate.PairSemantics.raw9878 line 335
  73. def OAI.MUB6.Certificate.PairSemantics.raw9878step0 line 337
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9878 line 339
  75. def OAI.MUB6.Certificate.PairSemantics.raw9879 line 348
  76. def OAI.MUB6.Certificate.PairSemantics.raw9879step0 line 350
  77. def OAI.MUB6.Certificate.PairSemantics.raw9879step1 line 352
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9879 line 354
  79. def OAI.MUB6.Certificate.PairSemantics.raw9880 line 367
  80. def OAI.MUB6.Certificate.PairSemantics.raw9880step0 line 369
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9880 line 371
  82. def OAI.MUB6.Certificate.PairSemantics.raw9881 line 380
  83. def OAI.MUB6.Certificate.PairSemantics.raw9881step0 line 382
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9881 line 384
  85. def OAI.MUB6.Certificate.PairSemantics.raw9882 line 393
  86. def OAI.MUB6.Certificate.PairSemantics.raw9882step0 line 395
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9882 line 397
  88. def OAI.MUB6.Certificate.PairSemantics.raw9883 line 406
  89. def OAI.MUB6.Certificate.PairSemantics.raw9883step0 line 408
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical9883 line 410
  91. def OAI.MUB6.Certificate.PairSemantics.raw9884 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw9884step0 line 421
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9884 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw9885 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw9885step0 line 434
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9885 line 436
  97. def OAI.MUB6.Certificate.PairSemantics.raw9886 line 445
  98. def OAI.MUB6.Certificate.PairSemantics.raw9886step0 line 447
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9886 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw9887 line 458
  101. def OAI.MUB6.Certificate.PairSemantics.raw9887step0 line 460
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9887 line 462