OAI/Analysis/CharacterCriterion/NoncommutingPair.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.sum_commutator line 18
2. lemma OAI.KirchbergRordam.GenericRW.commute_of_basis line 40
3. lemma OAI.KirchbergRordam.GenericRW.NoncommutingPair.mem_factor_commutant line 67
4. lemma OAI.KirchbergRordam.GenericRW.NoncommutingPair.selfAdjoint_sum line 73
5. lemma OAI.KirchbergRordam.GenericRW.NoncommutingPair.selfAdjoint_mul_of_commute line 78
6. lemma OAI.KirchbergRordam.GenericRW.NoncommutingPair.map_sum_mul line 82
7. theorem OAI.KirchbergRordam.GenericRW.NoncommutingPair.exists_pair line 88