OAI/Analysis/Pureness/GroupAlgebra/ReducedFreeGroupAWEmbedding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.reducedFreeGroupAWEmbedding line 13
2. lemma OAI.CuntzPureness.reducedFreeGroupAWEmbedding_injective line 18
3. lemma OAI.CuntzPureness.reducedFreeGroupAWEmbedding_isometry line 23
4. lemma OAI.CuntzPureness.reducedFreeGroupAWEmbedding_commute line 28
5. lemma OAI.CuntzPureness.reducedFreeGroupAWEmbedding_value line 34
6. def OAI.CuntzPureness.originalFreeGroupTensorHom line 41
7. lemma OAI.CuntzPureness.originalFreeGroupTensorHom_injective line 48
8. lemma OAI.CuntzPureness.originalFreeGroupTensorHom_left line 54
9. lemma OAI.CuntzPureness.originalFreeGroupTensorHom_right line 62