OAI/Analysis/Commutator/ChoiFunctional.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.OperatorSystem.CoordinateSpace line 24
2. def OAI.Kadison.OperatorSystem.basisVector line 26
3. lemma OAI.Kadison.OperatorSystem.basisVector_apply line 28
4. def OAI.Kadison.OperatorSystem.choi line 30
5. lemma OAI.Kadison.OperatorSystem.choi_nonneg line 36
6. theorem OAI.Kadison.OperatorSystem.exists_choi_extension line 47