OAI/Analysis/Pureness/GroupAlgebra/FiniteQuotientInclusions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.finiteQuotientQuasitrace line 14
2. lemma OAI.CuntzPureness.finiteQuotientQuasitrace_eq line 19
3. def OAI.CuntzPureness.finiteQuotientInclusion line 23
4. lemma OAI.CuntzPureness.finiteQuotientInclusion_embedding line 32
5. lemma OAI.CuntzPureness.finiteQuotientInclusion_value line 36
6. lemma OAI.CuntzPureness.finiteQuotientInclusion_isometry line 44
7. lemma OAI.CuntzPureness.finiteQuotientInclusion_self line 50
8. lemma OAI.CuntzPureness.finiteQuotientInclusion_trans line 61