OAI/Analysis/Commutator/PairTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.Pairing.Representatives line 21
2. theorem OAI.Kadison.Pairing.repr_representative line 23
3. def OAI.Kadison.Pairing.pairEquiv line 26
4. theorem OAI.Kadison.Pairing.pairEquiv_false line 48
5. theorem OAI.Kadison.Pairing.pairEquiv_true line 51
6. theorem OAI.Kadison.Pairing.prod_pairs line 54
7. def OAI.Kadison.Pairing.pairFunctionEquiv line 64
8. theorem OAI.Kadison.Pairing.pairFunctionEquiv_apply line 69
9. theorem OAI.Kadison.Pairing.sum_prod_pairs line 73