OAI/Analysis/Pureness/Stabilization/FamilyQuotient.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.FamilyQuotient line 11
2. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 15) line 15
3. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 17) line 17
4. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 19) line 19
5. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 21) line 21
6. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 23) line 23
7. def OAI.CuntzTrace.FamilyQuotient.mk line 26
8. lemma OAI.CuntzTrace.FamilyQuotient.mk_add line 27
9. lemma OAI.CuntzTrace.FamilyQuotient.mk_mul line 28
10. lemma OAI.CuntzTrace.FamilyQuotient.mk_sub line 29
11. lemma OAI.CuntzTrace.FamilyQuotient.mk_smul line 30
12. lemma OAI.CuntzTrace.FamilyQuotient.mk_zero line 31
13. lemma OAI.CuntzTrace.FamilyQuotient.mk_surjective line 32
14. lemma OAI.CuntzTrace.FamilyQuotient.mk_eq_mk_iff line 33
15. lemma OAI.CuntzTrace.FamilyQuotient.norm_mk_le line 35
16. lemma OAI.CuntzTrace.FamilyQuotient.exists_norm_mk_lt line 36
17. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 39) line 39
18. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 53) line 53
19. lemma OAI.CuntzTrace.FamilyQuotient.mk_star line 59
20. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 60) line 60
21. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 75) line 75
22. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 80) line 80
23. instance OAI.CuntzTrace.FamilyQuotient.(instance at line 86) line 86