OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical223.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7136 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw7136step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw7136step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7136 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw7137 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw7137step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw7137step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7137 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw7138 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw7138step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw7138step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7138 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw7139 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw7139step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw7139step1 line 80
  16. def OAI.MUB6.Certificate.PairSemantics.raw7139step2 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7139 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw7140 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw7140step0 line 103
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7140 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw7141 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw7141step0 line 116
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7141 line 118
  24. def OAI.MUB6.Certificate.PairSemantics.raw7142 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw7142step0 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw7142step1 line 131
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7142 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw7143 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw7143step0 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw7143step1 line 150
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7143 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw7144 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw7144step0 line 167
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7144 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw7145 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw7145step0 line 180
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical7145 line 182
  38. def OAI.MUB6.Certificate.PairSemantics.raw7146 line 191
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7146 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw7147 line 197
  41. def OAI.MUB6.Certificate.PairSemantics.raw7147step0 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw7147step1 line 201
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7147 line 203
  44. def OAI.MUB6.Certificate.PairSemantics.raw7148 line 216
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7148 line 218
  46. def OAI.MUB6.Certificate.PairSemantics.raw7149 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw7149step0 line 224
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7149 line 226
  49. def OAI.MUB6.Certificate.PairSemantics.raw7150 line 235
  50. def OAI.MUB6.Certificate.PairSemantics.raw7150step0 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw7150step1 line 239
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7150 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw7151 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw7151step0 line 256
  55. def OAI.MUB6.Certificate.PairSemantics.raw7151step1 line 258
  56. def OAI.MUB6.Certificate.PairSemantics.raw7151step2 line 260
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7151 line 262
  58. def OAI.MUB6.Certificate.PairSemantics.raw7152 line 279
  59. def OAI.MUB6.Certificate.PairSemantics.raw7152step0 line 281
  60. def OAI.MUB6.Certificate.PairSemantics.raw7152step1 line 283
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7152 line 285
  62. def OAI.MUB6.Certificate.PairSemantics.raw7153 line 298
  63. def OAI.MUB6.Certificate.PairSemantics.raw7153step0 line 300
  64. def OAI.MUB6.Certificate.PairSemantics.raw7153step1 line 302
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7153 line 304
  66. def OAI.MUB6.Certificate.PairSemantics.raw7154 line 317
  67. def OAI.MUB6.Certificate.PairSemantics.raw7154step0 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw7154step1 line 321
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7154 line 323
  70. def OAI.MUB6.Certificate.PairSemantics.raw7155 line 336
  71. def OAI.MUB6.Certificate.PairSemantics.raw7155step0 line 338
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7155 line 340
  73. def OAI.MUB6.Certificate.PairSemantics.raw7156 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw7156step0 line 351
  75. def OAI.MUB6.Certificate.PairSemantics.raw7156step1 line 353
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7156 line 355
  77. def OAI.MUB6.Certificate.PairSemantics.raw7157 line 368
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7157 line 370
  79. def OAI.MUB6.Certificate.PairSemantics.raw7158 line 374
  80. def OAI.MUB6.Certificate.PairSemantics.raw7158step0 line 376
  81. def OAI.MUB6.Certificate.PairSemantics.raw7158step1 line 378
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7158 line 380
  83. def OAI.MUB6.Certificate.PairSemantics.raw7159 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw7159step0 line 395
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7159 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw7160 line 406
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7160 line 408
  88. def OAI.MUB6.Certificate.PairSemantics.raw7161 line 412
  89. def OAI.MUB6.Certificate.PairSemantics.raw7161step0 line 414
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical7161 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw7162 line 425
  92. def OAI.MUB6.Certificate.PairSemantics.raw7162step0 line 427
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7162 line 429
  94. def OAI.MUB6.Certificate.PairSemantics.raw7163 line 438
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7163 line 440
  96. def OAI.MUB6.Certificate.PairSemantics.raw7164 line 444
  97. def OAI.MUB6.Certificate.PairSemantics.raw7164step0 line 446
  98. def OAI.MUB6.Certificate.PairSemantics.raw7164step1 line 448
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7164 line 450
  100. def OAI.MUB6.Certificate.PairSemantics.raw7165 line 463
  101. def OAI.MUB6.Certificate.PairSemantics.raw7165step0 line 465
  102. def OAI.MUB6.Certificate.PairSemantics.raw7165step1 line 467
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7165 line 469
  104. def OAI.MUB6.Certificate.PairSemantics.raw7166 line 482
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7166 line 484
  106. def OAI.MUB6.Certificate.PairSemantics.raw7167 line 488
  107. def OAI.MUB6.Certificate.PairSemantics.raw7167step0 line 490
  108. def OAI.MUB6.Certificate.PairSemantics.raw7167step1 line 492
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical7167 line 494