OAI/Analysis/Commutator/OperatorSystem.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorSystem.matrices line 20
2. lemma OAI.Kadison.OperatorSystem.matrices_mem line 27
3. lemma OAI.Kadison.OperatorSystem.matrices_one line 31
4. lemma OAI.Kadison.OperatorSystem.matrices_star line 38
5. def OAI.Kadison.OperatorSystem.mapMatrix line 42
6. lemma OAI.Kadison.OperatorSystem.mapMatrix_apply line 55
7. def OAI.Kadison.OperatorSystem.IsCompletelyPositive line 59