OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical309.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9888 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw9888step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9888 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw9889 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw9889step0 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw9889step1 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical9889 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw9890 line 50
  9. def OAI.MUB6.Certificate.PairSemantics.raw9890step0 line 52
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9890 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw9891 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw9891step0 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw9891step1 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical9891 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw9892 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw9892step0 line 84
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9892 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw9893 line 95
  19. def OAI.MUB6.Certificate.PairSemantics.raw9893step0 line 97
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical9893 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw9894 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw9894step0 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9894 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw9895 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw9895step0 line 123
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9895 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw9896 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw9896step0 line 136
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9896 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw9897 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw9897step0 line 149
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical9897 line 151
  33. def OAI.MUB6.Certificate.PairSemantics.raw9898 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw9898step0 line 162
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9898 line 164
  36. def OAI.MUB6.Certificate.PairSemantics.raw9899 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw9899step0 line 175
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9899 line 177
  39. def OAI.MUB6.Certificate.PairSemantics.raw9900 line 186
  40. def OAI.MUB6.Certificate.PairSemantics.raw9900step0 line 188
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9900 line 190
  42. def OAI.MUB6.Certificate.PairSemantics.raw9901 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw9901step0 line 201
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9901 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw9902 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw9902step0 line 214
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9902 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw9903 line 225
  49. def OAI.MUB6.Certificate.PairSemantics.raw9903step0 line 227
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9903 line 229
  51. def OAI.MUB6.Certificate.PairSemantics.raw9904 line 238
  52. def OAI.MUB6.Certificate.PairSemantics.raw9904step0 line 240
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9904 line 242
  54. def OAI.MUB6.Certificate.PairSemantics.raw9905 line 251
  55. def OAI.MUB6.Certificate.PairSemantics.raw9905step0 line 253
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9905 line 255
  57. def OAI.MUB6.Certificate.PairSemantics.raw9906 line 264
  58. def OAI.MUB6.Certificate.PairSemantics.raw9906step0 line 266
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9906 line 268
  60. def OAI.MUB6.Certificate.PairSemantics.raw9907 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw9907step0 line 279
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9907 line 281
  63. def OAI.MUB6.Certificate.PairSemantics.raw9908 line 290
  64. def OAI.MUB6.Certificate.PairSemantics.raw9908step0 line 292
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9908 line 294
  66. def OAI.MUB6.Certificate.PairSemantics.raw9909 line 303
  67. def OAI.MUB6.Certificate.PairSemantics.raw9909step0 line 305
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9909 line 307
  69. def OAI.MUB6.Certificate.PairSemantics.raw9910 line 316
  70. def OAI.MUB6.Certificate.PairSemantics.raw9910step0 line 318
  71. def OAI.MUB6.Certificate.PairSemantics.raw9910step1 line 320
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9910 line 322
  73. def OAI.MUB6.Certificate.PairSemantics.raw9911 line 335
  74. def OAI.MUB6.Certificate.PairSemantics.raw9911step0 line 337
  75. def OAI.MUB6.Certificate.PairSemantics.raw9911step1 line 339
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical9911 line 341
  77. def OAI.MUB6.Certificate.PairSemantics.raw9912 line 354
  78. def OAI.MUB6.Certificate.PairSemantics.raw9912step0 line 356
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical9912 line 358
  80. def OAI.MUB6.Certificate.PairSemantics.raw9913 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw9913step0 line 369
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9913 line 371
  83. def OAI.MUB6.Certificate.PairSemantics.raw9914 line 380
  84. def OAI.MUB6.Certificate.PairSemantics.raw9914step0 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw9914step1 line 384
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9914 line 386
  87. def OAI.MUB6.Certificate.PairSemantics.raw9915 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw9915step0 line 401
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9915 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw9916 line 412
  91. def OAI.MUB6.Certificate.PairSemantics.raw9916step0 line 414
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9916 line 416
  93. def OAI.MUB6.Certificate.PairSemantics.raw9917 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw9917step0 line 427
  95. def OAI.MUB6.Certificate.PairSemantics.raw9917step1 line 429
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical9917 line 431
  97. def OAI.MUB6.Certificate.PairSemantics.raw9918 line 445
  98. def OAI.MUB6.Certificate.PairSemantics.raw9918step0 line 447
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9918 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw9919 line 458
  101. def OAI.MUB6.Certificate.PairSemantics.raw9919step0 line 460
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9919 line 462