OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical170.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5440 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw5440step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw5440step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5440 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw5441 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw5441step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw5441step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5441 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw5442 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw5442step0 line 59
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5442 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw5443 line 70
  13. def OAI.MUB6.Certificate.PairSemantics.raw5443step0 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw5443step1 line 74
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5443 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw5444 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw5444step0 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw5444step1 line 93
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5444 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw5445 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw5445step0 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw5445step1 line 112
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5445 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw5446 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw5446step0 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw5446step1 line 131
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5446 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw5447 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw5447step0 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw5447step1 line 150
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5447 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw5448 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw5448step0 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw5448step1 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw5448step2 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5448 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw5449 line 190
  38. def OAI.MUB6.Certificate.PairSemantics.raw5449step0 line 192
  39. def OAI.MUB6.Certificate.PairSemantics.raw5449step1 line 194
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5449 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw5450 line 209
  42. def OAI.MUB6.Certificate.PairSemantics.raw5450step0 line 211
  43. def OAI.MUB6.Certificate.PairSemantics.raw5450step1 line 213
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5450 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw5451 line 228
  46. def OAI.MUB6.Certificate.PairSemantics.raw5451step0 line 230
  47. def OAI.MUB6.Certificate.PairSemantics.raw5451step1 line 232
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5451 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw5452 line 247
  50. def OAI.MUB6.Certificate.PairSemantics.raw5452step0 line 249
  51. def OAI.MUB6.Certificate.PairSemantics.raw5452step1 line 251
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5452 line 253
  53. def OAI.MUB6.Certificate.PairSemantics.raw5453 line 266
  54. def OAI.MUB6.Certificate.PairSemantics.raw5453step0 line 268
  55. def OAI.MUB6.Certificate.PairSemantics.raw5453step1 line 270
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5453 line 272
  57. def OAI.MUB6.Certificate.PairSemantics.raw5454 line 285
  58. def OAI.MUB6.Certificate.PairSemantics.raw5454step0 line 287
  59. def OAI.MUB6.Certificate.PairSemantics.raw5454step1 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw5454step2 line 291
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5454 line 293
  62. def OAI.MUB6.Certificate.PairSemantics.raw5455 line 310
  63. def OAI.MUB6.Certificate.PairSemantics.raw5455step0 line 312
  64. def OAI.MUB6.Certificate.PairSemantics.raw5455step1 line 314
  65. def OAI.MUB6.Certificate.PairSemantics.raw5455step2 line 316
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5455 line 318
  67. def OAI.MUB6.Certificate.PairSemantics.raw5456 line 335
  68. def OAI.MUB6.Certificate.PairSemantics.raw5456step0 line 337
  69. def OAI.MUB6.Certificate.PairSemantics.raw5456step1 line 339
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical5456 line 341
  71. def OAI.MUB6.Certificate.PairSemantics.raw5457 line 354
  72. def OAI.MUB6.Certificate.PairSemantics.raw5457step0 line 356
  73. def OAI.MUB6.Certificate.PairSemantics.raw5457step1 line 358
  74. def OAI.MUB6.Certificate.PairSemantics.raw5457step2 line 360
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5457 line 362
  76. def OAI.MUB6.Certificate.PairSemantics.raw5458 line 379
  77. def OAI.MUB6.Certificate.PairSemantics.raw5458step0 line 381
  78. def OAI.MUB6.Certificate.PairSemantics.raw5458step1 line 383
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5458 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw5459 line 398
  81. def OAI.MUB6.Certificate.PairSemantics.raw5459step0 line 400
  82. def OAI.MUB6.Certificate.PairSemantics.raw5459step1 line 402
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5459 line 404
  84. def OAI.MUB6.Certificate.PairSemantics.raw5460 line 417
  85. def OAI.MUB6.Certificate.PairSemantics.raw5460step0 line 419
  86. def OAI.MUB6.Certificate.PairSemantics.raw5460step1 line 421
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5460 line 423
  88. def OAI.MUB6.Certificate.PairSemantics.raw5461 line 436
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5461 line 438
  90. def OAI.MUB6.Certificate.PairSemantics.raw5462 line 442
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5462 line 444
  92. def OAI.MUB6.Certificate.PairSemantics.raw5463 line 448
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5463 line 450
  94. def OAI.MUB6.Certificate.PairSemantics.raw5464 line 454
  95. def OAI.MUB6.Certificate.PairSemantics.raw5464step0 line 456
  96. def OAI.MUB6.Certificate.PairSemantics.raw5464step1 line 458
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5464 line 460
  98. def OAI.MUB6.Certificate.PairSemantics.raw5465 line 473
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5465 line 475
  100. def OAI.MUB6.Certificate.PairSemantics.raw5466 line 479
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical5466 line 481
  102. def OAI.MUB6.Certificate.PairSemantics.raw5467 line 485
  103. def OAI.MUB6.Certificate.PairSemantics.raw5467step0 line 487
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical5467 line 489
  105. def OAI.MUB6.Certificate.PairSemantics.raw5468 line 498
  106. def OAI.MUB6.Certificate.PairSemantics.raw5468step0 line 500
  107. def OAI.MUB6.Certificate.PairSemantics.raw5468step1 line 502
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical5468 line 504
  109. def OAI.MUB6.Certificate.PairSemantics.raw5469 line 517
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5469 line 519
  111. def OAI.MUB6.Certificate.PairSemantics.raw5470 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw5470step0 line 525
  113. def OAI.MUB6.Certificate.PairSemantics.raw5470step1 line 527
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical5470 line 529
  115. def OAI.MUB6.Certificate.PairSemantics.raw5471 line 542
  116. def OAI.MUB6.Certificate.PairSemantics.raw5471step0 line 544
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical5471 line 546