OAI/Analysis/Commutator/CrossingPairings.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.Pairing.Crosses line 22
2. def OAI.Kadison.Pairing.crossPairing line 26
3. theorem OAI.Kadison.Pairing.crossPairing_inl line 46
4. theorem OAI.Kadison.Pairing.crossPairing_inr line 49
5. theorem OAI.Kadison.Pairing.crossPairing_crosses line 52
6. theorem OAI.Kadison.Pairing.crossPairing_injective line 56
7. theorem OAI.Kadison.Pairing.exists_crossPairing line 63
8. def OAI.Kadison.Pairing.crossingEquiv line 91
9. theorem OAI.Kadison.Pairing.crossingEquiv_val line 98
10. theorem OAI.Kadison.Pairing.contraction_crossPairing line 101
11. theorem OAI.Kadison.Pairing.sum_contraction_crossing line 115