OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical179.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5728 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw5728step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw5728step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5728 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw5729 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw5729step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw5729step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5729 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw5730 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw5730step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw5730step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5730 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw5731 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw5731step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw5731step1 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw5731step2 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5731 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw5732 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw5732step0 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw5732step1 line 105
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5732 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw5733 line 120
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5733 line 122
  24. def OAI.MUB6.Certificate.PairSemantics.raw5734 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw5734step0 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw5734step1 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5734 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw5735 line 145
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5735 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw5736 line 151
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5736 line 153
  32. def OAI.MUB6.Certificate.PairSemantics.raw5737 line 157
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5737 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw5738 line 163
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5738 line 165
  36. def OAI.MUB6.Certificate.PairSemantics.raw5739 line 169
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical5739 line 171
  38. def OAI.MUB6.Certificate.PairSemantics.raw5740 line 175
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5740 line 177
  40. def OAI.MUB6.Certificate.PairSemantics.raw5741 line 181
  41. def OAI.MUB6.Certificate.PairSemantics.raw5741step0 line 183
  42. def OAI.MUB6.Certificate.PairSemantics.raw5741step1 line 185
  43. def OAI.MUB6.Certificate.PairSemantics.raw5741step2 line 187
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5741 line 189
  45. def OAI.MUB6.Certificate.PairSemantics.raw5742 line 206
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5742 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw5743 line 212
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5743 line 214
  49. def OAI.MUB6.Certificate.PairSemantics.raw5744 line 218
  50. def OAI.MUB6.Certificate.PairSemantics.raw5744step0 line 220
  51. def OAI.MUB6.Certificate.PairSemantics.raw5744step1 line 222
  52. def OAI.MUB6.Certificate.PairSemantics.raw5744step2 line 224
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5744 line 226
  54. def OAI.MUB6.Certificate.PairSemantics.raw5745 line 244
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5745 line 246
  56. def OAI.MUB6.Certificate.PairSemantics.raw5746 line 250
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical5746 line 252
  58. def OAI.MUB6.Certificate.PairSemantics.raw5747 line 256
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5747 line 258
  60. def OAI.MUB6.Certificate.PairSemantics.raw5748 line 262
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5748 line 264
  62. def OAI.MUB6.Certificate.PairSemantics.raw5749 line 268
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5749 line 270
  64. def OAI.MUB6.Certificate.PairSemantics.raw5750 line 274
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5750 line 276
  66. def OAI.MUB6.Certificate.PairSemantics.raw5751 line 280
  67. def OAI.MUB6.Certificate.PairSemantics.raw5751step0 line 282
  68. def OAI.MUB6.Certificate.PairSemantics.raw5751step1 line 284
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5751 line 286
  70. def OAI.MUB6.Certificate.PairSemantics.raw5752 line 299
  71. def OAI.MUB6.Certificate.PairSemantics.raw5752step0 line 301
  72. def OAI.MUB6.Certificate.PairSemantics.raw5752step1 line 303
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5752 line 305
  74. def OAI.MUB6.Certificate.PairSemantics.raw5753 line 318
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5753 line 320
  76. def OAI.MUB6.Certificate.PairSemantics.raw5754 line 324
  77. def OAI.MUB6.Certificate.PairSemantics.raw5754step0 line 326
  78. def OAI.MUB6.Certificate.PairSemantics.raw5754step1 line 328
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5754 line 330
  80. def OAI.MUB6.Certificate.PairSemantics.raw5755 line 343
  81. def OAI.MUB6.Certificate.PairSemantics.raw5755step0 line 345
  82. def OAI.MUB6.Certificate.PairSemantics.raw5755step1 line 347
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5755 line 349
  84. def OAI.MUB6.Certificate.PairSemantics.raw5756 line 362
  85. def OAI.MUB6.Certificate.PairSemantics.raw5756step0 line 364
  86. def OAI.MUB6.Certificate.PairSemantics.raw5756step1 line 366
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5756 line 368
  88. def OAI.MUB6.Certificate.PairSemantics.raw5757 line 381
  89. def OAI.MUB6.Certificate.PairSemantics.raw5757step0 line 383
  90. def OAI.MUB6.Certificate.PairSemantics.raw5757step1 line 385
  91. def OAI.MUB6.Certificate.PairSemantics.raw5757step2 line 387
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical5757 line 389
  93. def OAI.MUB6.Certificate.PairSemantics.raw5758 line 407
  94. def OAI.MUB6.Certificate.PairSemantics.raw5758step0 line 409
  95. def OAI.MUB6.Certificate.PairSemantics.raw5758step1 line 411
  96. def OAI.MUB6.Certificate.PairSemantics.raw5758step2 line 413
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5758 line 415
  98. def OAI.MUB6.Certificate.PairSemantics.raw5759 line 433
  99. def OAI.MUB6.Certificate.PairSemantics.raw5759step0 line 435
  100. def OAI.MUB6.Certificate.PairSemantics.raw5759step1 line 437
  101. def OAI.MUB6.Certificate.PairSemantics.raw5759step2 line 439
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical5759 line 441