OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical141.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4512 line 19
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4512 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw4513 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4513 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw4514 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw4514step0 line 33
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4514 line 35
  8. def OAI.MUB6.Certificate.PairSemantics.raw4515 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw4515step0 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4515 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw4516 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw4516step0 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw4516step1 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw4516step2 line 63
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical4516 line 65
  16. def OAI.MUB6.Certificate.PairSemantics.raw4517 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4517 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw4518 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw4518step0 line 91
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4518 line 93
  21. def OAI.MUB6.Certificate.PairSemantics.raw4519 line 102
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4519 line 104
  23. def OAI.MUB6.Certificate.PairSemantics.raw4520 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw4520step0 line 110
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4520 line 112
  26. def OAI.MUB6.Certificate.PairSemantics.raw4521 line 121
  27. def OAI.MUB6.Certificate.PairSemantics.raw4521step0 line 123
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4521 line 125
  29. def OAI.MUB6.Certificate.PairSemantics.raw4522 line 134
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4522 line 136
  31. def OAI.MUB6.Certificate.PairSemantics.raw4523 line 140
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4523 line 142
  33. def OAI.MUB6.Certificate.PairSemantics.raw4524 line 146
  34. def OAI.MUB6.Certificate.PairSemantics.raw4524step0 line 148
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4524 line 150
  36. def OAI.MUB6.Certificate.PairSemantics.raw4525 line 159
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4525 line 161
  38. def OAI.MUB6.Certificate.PairSemantics.raw4526 line 165
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4526 line 167
  40. def OAI.MUB6.Certificate.PairSemantics.raw4527 line 171
  41. def OAI.MUB6.Certificate.PairSemantics.raw4527step0 line 173
  42. def OAI.MUB6.Certificate.PairSemantics.raw4527step1 line 175
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4527 line 177
  44. def OAI.MUB6.Certificate.PairSemantics.raw4528 line 190
  45. def OAI.MUB6.Certificate.PairSemantics.raw4528step0 line 192
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4528 line 194
  47. def OAI.MUB6.Certificate.PairSemantics.raw4529 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw4529step0 line 205
  49. def OAI.MUB6.Certificate.PairSemantics.raw4529step1 line 207
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4529 line 209
  51. def OAI.MUB6.Certificate.PairSemantics.raw4530 line 222
  52. def OAI.MUB6.Certificate.PairSemantics.raw4530step0 line 224
  53. def OAI.MUB6.Certificate.PairSemantics.raw4530step1 line 226
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4530 line 228
  55. def OAI.MUB6.Certificate.PairSemantics.raw4531 line 241
  56. def OAI.MUB6.Certificate.PairSemantics.raw4531step0 line 243
  57. def OAI.MUB6.Certificate.PairSemantics.raw4531step1 line 245
  58. def OAI.MUB6.Certificate.PairSemantics.raw4531step2 line 247
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4531 line 249
  60. def OAI.MUB6.Certificate.PairSemantics.raw4532 line 266
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4532 line 268
  62. def OAI.MUB6.Certificate.PairSemantics.raw4533 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw4533step0 line 274
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4533 line 276
  65. def OAI.MUB6.Certificate.PairSemantics.raw4534 line 285
  66. def OAI.MUB6.Certificate.PairSemantics.raw4534step0 line 287
  67. def OAI.MUB6.Certificate.PairSemantics.raw4534step1 line 289
  68. def OAI.MUB6.Certificate.PairSemantics.raw4534step2 line 291
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4534 line 293
  70. def OAI.MUB6.Certificate.PairSemantics.raw4535 line 310
  71. def OAI.MUB6.Certificate.PairSemantics.raw4535step0 line 312
  72. def OAI.MUB6.Certificate.PairSemantics.raw4535step1 line 314
  73. def OAI.MUB6.Certificate.PairSemantics.raw4535step2 line 316
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4535 line 318
  75. def OAI.MUB6.Certificate.PairSemantics.raw4536 line 335
  76. def OAI.MUB6.Certificate.PairSemantics.raw4536step0 line 337
  77. def OAI.MUB6.Certificate.PairSemantics.raw4536step1 line 339
  78. def OAI.MUB6.Certificate.PairSemantics.raw4536step2 line 341
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4536 line 343
  80. def OAI.MUB6.Certificate.PairSemantics.raw4537 line 360
  81. def OAI.MUB6.Certificate.PairSemantics.raw4537step0 line 362
  82. def OAI.MUB6.Certificate.PairSemantics.raw4537step1 line 364
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4537 line 366
  84. def OAI.MUB6.Certificate.PairSemantics.raw4538 line 379
  85. def OAI.MUB6.Certificate.PairSemantics.raw4538step0 line 381
  86. def OAI.MUB6.Certificate.PairSemantics.raw4538step1 line 383
  87. def OAI.MUB6.Certificate.PairSemantics.raw4538step2 line 385
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4538 line 387
  89. def OAI.MUB6.Certificate.PairSemantics.raw4539 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw4539step0 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw4539step1 line 408
  92. def OAI.MUB6.Certificate.PairSemantics.raw4539step2 line 410
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4539 line 412
  94. def OAI.MUB6.Certificate.PairSemantics.raw4540 line 429
  95. def OAI.MUB6.Certificate.PairSemantics.raw4540step0 line 431
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4540 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw4541 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw4541step0 line 444
  99. def OAI.MUB6.Certificate.PairSemantics.raw4541step1 line 446
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4541 line 448
  101. def OAI.MUB6.Certificate.PairSemantics.raw4542 line 461
  102. def OAI.MUB6.Certificate.PairSemantics.raw4542step0 line 463
  103. def OAI.MUB6.Certificate.PairSemantics.raw4542step1 line 465
  104. def OAI.MUB6.Certificate.PairSemantics.raw4542step2 line 467
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical4542 line 469
  106. def OAI.MUB6.Certificate.PairSemantics.raw4543 line 487
  107. def OAI.MUB6.Certificate.PairSemantics.raw4543step0 line 489
  108. def OAI.MUB6.Certificate.PairSemantics.raw4543step1 line 491
  109. def OAI.MUB6.Certificate.PairSemantics.raw4543step2 line 493
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical4543 line 495