OAI/Analysis/Pureness/GroupAlgebra/WordAncestorFactorization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.sum_diagonal_indicator line 10
2. lemma OAI.CuntzPureness.wordAncestorPair_nil_left line 26
3. lemma OAI.CuntzPureness.wordAncestorPair_symm line 43
4. theorem OAI.CuntzPureness.wordMeetKernel_eq_ancestor_sum line 48
5. def OAI.CuntzPureness.wordAncestorVector line 74
6. lemma OAI.CuntzPureness.wordAncestorVector_norm_le line 79
7. lemma OAI.CuntzPureness.wordAncestorVector_inner line 86
8. theorem OAI.CuntzPureness.wordMeetKernel_factorization line 92