OAI/Analysis/Pureness/GroupAlgebra/ResidualFiniteQuotientSequence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CuntzPureness.exists_separating_normal_sequence line 12
2. def OAI.CuntzPureness.separatingNormalSequence line 38
3. lemma OAI.CuntzPureness.separatingNormalSequence_antitone line 41
4. lemma OAI.CuntzPureness.separatingNormalSequence_eventually line 44
5. abbrev OAI.CuntzPureness.SeparatingFiniteQuotient line 48
6. def OAI.CuntzPureness.separatingQuotientMap line 50
7. instance OAI.CuntzPureness.separatingFiniteQuotient_finite line 53
8. lemma OAI.CuntzPureness.separatingQuotientMap_eventually_ne line 56
9. theorem OAI.CuntzPureness.separatingQuotientMap_eventually_injOn line 66
10. theorem OAI.CuntzPureness.freeGroup_nat_finite_quotients line 78