OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical98.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3136 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw3136step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw3136step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3136 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw3137 line 39
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical3137 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw3138 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw3138step0 line 47
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3138 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw3139 line 58
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3139 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw3140 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw3140step0 line 66
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3140 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw3141 line 77
  16. def OAI.MUB6.Certificate.PairSemantics.raw3141step0 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw3141step1 line 81
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3141 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw3142 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw3142step0 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3142 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw3143 line 109
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical3143 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw3144 line 115
  25. def OAI.MUB6.Certificate.PairSemantics.raw3144step0 line 117
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3144 line 119
  27. def OAI.MUB6.Certificate.PairSemantics.raw3145 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw3145step0 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw3145step1 line 132
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3145 line 134
  31. def OAI.MUB6.Certificate.PairSemantics.raw3146 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw3146step0 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw3146step1 line 151
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3146 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw3147 line 166
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3147 line 168
  37. def OAI.MUB6.Certificate.PairSemantics.raw3148 line 172
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3148 line 174
  39. def OAI.MUB6.Certificate.PairSemantics.raw3149 line 178
  40. def OAI.MUB6.Certificate.PairSemantics.raw3149step0 line 180
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3149 line 182
  42. def OAI.MUB6.Certificate.PairSemantics.raw3150 line 191
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3150 line 193
  44. def OAI.MUB6.Certificate.PairSemantics.raw3151 line 197
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3151 line 199
  46. def OAI.MUB6.Certificate.PairSemantics.raw3152 line 203
  47. def OAI.MUB6.Certificate.PairSemantics.raw3152step0 line 205
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3152 line 207
  49. def OAI.MUB6.Certificate.PairSemantics.raw3153 line 216
  50. def OAI.MUB6.Certificate.PairSemantics.raw3153step0 line 218
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3153 line 220
  52. def OAI.MUB6.Certificate.PairSemantics.raw3154 line 229
  53. def OAI.MUB6.Certificate.PairSemantics.raw3154step0 line 231
  54. def OAI.MUB6.Certificate.PairSemantics.raw3154step1 line 233
  55. def OAI.MUB6.Certificate.PairSemantics.raw3154step2 line 235
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3154 line 237
  57. def OAI.MUB6.Certificate.PairSemantics.raw3155 line 254
  58. def OAI.MUB6.Certificate.PairSemantics.raw3155step0 line 256
  59. def OAI.MUB6.Certificate.PairSemantics.raw3155step1 line 258
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical3155 line 260
  61. def OAI.MUB6.Certificate.PairSemantics.raw3156 line 273
  62. def OAI.MUB6.Certificate.PairSemantics.raw3156step0 line 275
  63. def OAI.MUB6.Certificate.PairSemantics.raw3156step1 line 277
  64. def OAI.MUB6.Certificate.PairSemantics.raw3156step2 line 279
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3156 line 281
  66. def OAI.MUB6.Certificate.PairSemantics.raw3157 line 298
  67. def OAI.MUB6.Certificate.PairSemantics.raw3157step0 line 300
  68. def OAI.MUB6.Certificate.PairSemantics.raw3157step1 line 302
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3157 line 304
  70. def OAI.MUB6.Certificate.PairSemantics.raw3158 line 317
  71. def OAI.MUB6.Certificate.PairSemantics.raw3158step0 line 319
  72. def OAI.MUB6.Certificate.PairSemantics.raw3158step1 line 321
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3158 line 323
  74. def OAI.MUB6.Certificate.PairSemantics.raw3159 line 336
  75. def OAI.MUB6.Certificate.PairSemantics.raw3159step0 line 338
  76. def OAI.MUB6.Certificate.PairSemantics.raw3159step1 line 340
  77. def OAI.MUB6.Certificate.PairSemantics.raw3159step2 line 342
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical3159 line 344
  79. def OAI.MUB6.Certificate.PairSemantics.raw3160 line 361
  80. def OAI.MUB6.Certificate.PairSemantics.raw3160step0 line 363
  81. def OAI.MUB6.Certificate.PairSemantics.raw3160step1 line 365
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3160 line 367
  83. def OAI.MUB6.Certificate.PairSemantics.raw3161 line 380
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3161 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw3162 line 386
  86. def OAI.MUB6.Certificate.PairSemantics.raw3162step0 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw3162step1 line 390
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical3162 line 392
  89. def OAI.MUB6.Certificate.PairSemantics.raw3163 line 405
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3163 line 407
  91. def OAI.MUB6.Certificate.PairSemantics.raw3164 line 411
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3164 line 413
  93. def OAI.MUB6.Certificate.PairSemantics.raw3165 line 417
  94. def OAI.MUB6.Certificate.PairSemantics.raw3165step0 line 419
  95. def OAI.MUB6.Certificate.PairSemantics.raw3165step1 line 421
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3165 line 423
  97. def OAI.MUB6.Certificate.PairSemantics.raw3166 line 436
  98. def OAI.MUB6.Certificate.PairSemantics.raw3166step0 line 438
  99. def OAI.MUB6.Certificate.PairSemantics.raw3166step1 line 440
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3166 line 442
  101. def OAI.MUB6.Certificate.PairSemantics.raw3167 line 455
  102. def OAI.MUB6.Certificate.PairSemantics.raw3167step0 line 457
  103. def OAI.MUB6.Certificate.PairSemantics.raw3167step1 line 459
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3167 line 461