OAI/Analysis/Pureness/States/FiniteFamilyFreeGroup.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.reducedFreeGroupAWEmbedding line 15
2. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.reducedFreeGroupAWEmbedding_injective line 20
3. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.reducedFreeGroupAWEmbedding_isometry line 25
4. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.reducedFreeGroupAWEmbedding_commute line 30
5. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.reducedFreeGroupAWEmbedding_value line 36
6. def OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupTensorHom line 43
7. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupTensorHom_injective line 50
8. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupTensorHom_left line 56
9. lemma OAI.CuntzPureness.CompatibleFiniteQuasitrace.originalFreeGroupTensorHom_right line 64