OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical15.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw480 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw480step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw480step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical480 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw481 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw481step0 line 39
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical481 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw482 line 50
  9. def OAI.MUB6.Certificate.PairSemantics.raw482step0 line 52
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical482 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw483 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw483step0 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw483step1 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical483 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw484 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw484step0 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw484step1 line 86
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical484 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw485 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw485step0 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw485step1 line 105
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical485 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw486 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw486step0 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw486step1 line 124
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical486 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw487 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw487step0 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw487step1 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw487step2 line 145
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical487 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw488 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw488step0 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw488step1 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw488step2 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical488 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw489 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw489step0 line 193
  39. def OAI.MUB6.Certificate.PairSemantics.raw489step1 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw489step2 line 197
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical489 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw490 line 217
  43. def OAI.MUB6.Certificate.PairSemantics.raw490step0 line 219
  44. def OAI.MUB6.Certificate.PairSemantics.raw490step1 line 221
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical490 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw491 line 236
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical491 line 238
  48. def OAI.MUB6.Certificate.PairSemantics.raw492 line 242
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical492 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw493 line 248
  51. def OAI.MUB6.Certificate.PairSemantics.raw493step0 line 250
  52. def OAI.MUB6.Certificate.PairSemantics.raw493step1 line 252
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical493 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw494 line 267
  55. def OAI.MUB6.Certificate.PairSemantics.raw494step0 line 269
  56. def OAI.MUB6.Certificate.PairSemantics.raw494step1 line 271
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical494 line 273
  58. def OAI.MUB6.Certificate.PairSemantics.raw495 line 286
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical495 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw496 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw496step0 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw496step1 line 296
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical496 line 298
  64. def OAI.MUB6.Certificate.PairSemantics.raw497 line 311
  65. def OAI.MUB6.Certificate.PairSemantics.raw497step0 line 313
  66. def OAI.MUB6.Certificate.PairSemantics.raw497step1 line 315
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical497 line 317
  68. def OAI.MUB6.Certificate.PairSemantics.raw498 line 330
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical498 line 332
  70. def OAI.MUB6.Certificate.PairSemantics.raw499 line 336
  71. def OAI.MUB6.Certificate.PairSemantics.raw499step0 line 338
  72. def OAI.MUB6.Certificate.PairSemantics.raw499step1 line 340
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical499 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw500 line 355
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical500 line 357
  76. def OAI.MUB6.Certificate.PairSemantics.raw501 line 361
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical501 line 363
  78. def OAI.MUB6.Certificate.PairSemantics.raw502 line 367
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical502 line 369
  80. def OAI.MUB6.Certificate.PairSemantics.raw503 line 373
  81. def OAI.MUB6.Certificate.PairSemantics.raw503step0 line 375
  82. def OAI.MUB6.Certificate.PairSemantics.raw503step1 line 377
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical503 line 379
  84. def OAI.MUB6.Certificate.PairSemantics.raw504 line 392
  85. def OAI.MUB6.Certificate.PairSemantics.raw504step0 line 394
  86. def OAI.MUB6.Certificate.PairSemantics.raw504step1 line 396
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical504 line 398
  88. def OAI.MUB6.Certificate.PairSemantics.raw505 line 411
  89. def OAI.MUB6.Certificate.PairSemantics.raw505step0 line 413
  90. def OAI.MUB6.Certificate.PairSemantics.raw505step1 line 415
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical505 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw506 line 430
  93. def OAI.MUB6.Certificate.PairSemantics.raw506step0 line 432
  94. def OAI.MUB6.Certificate.PairSemantics.raw506step1 line 434
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical506 line 436
  96. def OAI.MUB6.Certificate.PairSemantics.raw507 line 449
  97. def OAI.MUB6.Certificate.PairSemantics.raw507step0 line 451
  98. def OAI.MUB6.Certificate.PairSemantics.raw507step1 line 453
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical507 line 455
  100. def OAI.MUB6.Certificate.PairSemantics.raw508 line 469
  101. def OAI.MUB6.Certificate.PairSemantics.raw508step0 line 471
  102. def OAI.MUB6.Certificate.PairSemantics.raw508step1 line 473
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical508 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw509 line 489
  105. def OAI.MUB6.Certificate.PairSemantics.raw509step0 line 491
  106. def OAI.MUB6.Certificate.PairSemantics.raw509step1 line 493
  107. def OAI.MUB6.Certificate.PairSemantics.raw509step2 line 495
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical509 line 497
  109. def OAI.MUB6.Certificate.PairSemantics.raw510 line 515
  110. def OAI.MUB6.Certificate.PairSemantics.raw510step0 line 517
  111. def OAI.MUB6.Certificate.PairSemantics.raw510step1 line 519
  112. def OAI.MUB6.Certificate.PairSemantics.raw510step2 line 521
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical510 line 523
  114. def OAI.MUB6.Certificate.PairSemantics.raw511 line 541
  115. def OAI.MUB6.Certificate.PairSemantics.raw511step0 line 543
  116. def OAI.MUB6.Certificate.PairSemantics.raw511step1 line 545
  117. def OAI.MUB6.Certificate.PairSemantics.raw511step2 line 547
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical511 line 549