OAI/Analysis/Pureness/GroupAlgebra/FreeWordTreeDistance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.wordTreeDistance line 8
2. lemma OAI.CuntzPureness.wordTreeDistance_self line 13
3. lemma OAI.CuntzPureness.wordTreeDistance_symm line 18
4. lemma OAI.CuntzPureness.reduced_invRev line 30
5. lemma OAI.CuntzPureness.reduced_invRev_append_of_heads_ne line 35
6. theorem OAI.CuntzPureness.reduced_word_distance line 51
7. theorem OAI.CuntzPureness.freeGroup_mul_inv_length line 82