OAI/Analysis/Pureness/GroupAlgebra/GroupCoordinateProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.groupCoordinateProjection line 10
2. lemma OAI.CuntzPureness.groupCoordinateProjection_apply line 29
3. lemma OAI.CuntzPureness.groupCoordinateProjection_norm_le line 32
4. lemma OAI.CuntzPureness.groupCoordinateProjection_star line 35
5. lemma OAI.CuntzPureness.groupCoordinateProjection_compl line 46
6. lemma OAI.CuntzPureness.groupCoordinateProjection_mul line 53
7. lemma OAI.CuntzPureness.groupCoordinateProjection_disjoint line 59
8. lemma OAI.CuntzPureness.groupCoordinateProjection_conjugate line 66
9. lemma OAI.CuntzPureness.groupCoordinateProjection_translation_zero line 78