OAI/Analysis/MutuallyUnbiased/PairSemantics/Boundary16.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal448 line 23
2. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix448 line 25
3. def OAI.MUB6.Certificate.PairSemantics.boundaryRow448 line 27
4. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound448 line 29
5. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal454 line 76
6. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix454 line 78
7. def OAI.MUB6.Certificate.PairSemantics.boundaryRow454 line 80
8. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound454 line 82
9. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal455 line 129
10. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix455 line 131
11. def OAI.MUB6.Certificate.PairSemantics.boundaryRow455 line 133
12. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound455 line 135
13. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal460 line 182
14. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix460 line 184
15. def OAI.MUB6.Certificate.PairSemantics.boundaryRow460 line 186
16. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound460 line 188
17. def OAI.MUB6.Certificate.PairSemantics.boundaryOriginal461 line 235
18. def OAI.MUB6.Certificate.PairSemantics.boundaryMatrix461 line 237
19. def OAI.MUB6.Certificate.PairSemantics.boundaryRow461 line 239
20. theorem OAI.MUB6.Certificate.PairSemantics.boundarySound461 line 241