OAI/Analysis/Commutator/Pairings.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.Pairing line 18
2. instance OAI.Kadison.Pairing.(instance at line 24) line 24
3. theorem OAI.Kadison.Pairing.apply_apply line 26
4. theorem OAI.Kadison.Pairing.apply_ne line 28
5. theorem OAI.Kadison.Pairing.injective line 30
6. theorem OAI.Kadison.Pairing.ext line 32
7. instance OAI.Kadison.Pairing.(instance at line 36) line 36
8. instance OAI.Kadison.Pairing.(instance at line 38) line 38
9. def OAI.Kadison.Pairing.repr line 42
10. theorem OAI.Kadison.Pairing.repr_apply line 44
11. theorem OAI.Kadison.Pairing.repr_eq_iff line 47
12. def OAI.Kadison.Pairing.labels line 66
13. theorem OAI.Kadison.Pairing.labels_eq_iff line 69
14. def OAI.Kadison.Pairing.contraction line 80
15. theorem OAI.Kadison.Pairing.pair_tests_iff line 84
16. theorem OAI.Kadison.Pairing.contraction_isolation line 95