OAI/Analysis/Commutator/ProjectionSumEquivalence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.PartialIsometryOrder.orthogonal_sum_projection line 21
2. lemma OAI.Kadison.PartialIsometryOrder.orthogonal_mul_sum_eq_zero line 39
3. lemma OAI.Kadison.PartialIsometryOrder.Equivalent.finset_sum line 47
4. lemma OAI.Kadison.PartialIsometryOrder.SubEquivalent.finset_sum line 61