OAI/Analysis/Pureness/GroupAlgebra/ReducedFreeGroupUltraEmbedding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzPureness.FreeGroupUltraGenerated line 12
2. def OAI.CuntzPureness.freeGroupUltraGeneratedTrace line 14
3. lemma OAI.CuntzPureness.freeGroupUltraGeneratedTrace_delta line 18
4. lemma OAI.CuntzPureness.freeGroupUltraGeneratedTrace_faithful line 22
5. def OAI.CuntzPureness.freeGroupUltraReducedEquiv line 28
6. def OAI.CuntzPureness.reducedFreeGroupUltraEmbedding line 34
7. lemma OAI.CuntzPureness.reducedFreeGroupUltraEmbedding_injective line 39
8. lemma OAI.CuntzPureness.reducedFreeGroupUltraEmbedding_isometry line 42
9. lemma OAI.CuntzPureness.reducedFreeGroupUltraEmbedding_trace line 46
10. lemma OAI.CuntzPureness.reducedFreeGroupUltraEmbedding_generator line 59
11. theorem OAI.CuntzPureness.reducedFreeGroup_exists_scalarUltraEmbedding line 74