OAI/Analysis/Pureness/GroupAlgebra/FreeGroupPowersPartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.freeGroupPowersC line 9
2. lemma OAI.CuntzPureness.reduced_append_of_old_new line 12
3. lemma OAI.CuntzPureness.freeGroup_old_mul_new_word line 24
4. theorem OAI.CuntzPureness.freeGroupPowersC_old_disjoint line 34
5. lemma OAI.CuntzPureness.freeGroup_fresh_mul_complement_word line 52
6. theorem OAI.CuntzPureness.freeGroupPowers_complement_images_disjoint line 66