OAI/Analysis/SeparableQuotients/Complexification.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.Complexify line 13
2. def OAI.SeparableQuotient.Complexify.toCLM line 15
3. instance OAI.SeparableQuotient.Complexify.(instance at line 16) line 16
4. lemma OAI.SeparableQuotient.Complexify.ext line 17
5. instance OAI.SeparableQuotient.Complexify.(instance at line 19) line 19
6. instance OAI.SeparableQuotient.Complexify.(instance at line 20) line 20
7. instance OAI.SeparableQuotient.Complexify.(instance at line 21) line 21
8. lemma OAI.SeparableQuotient.Complexify.add_apply line 23
9. lemma OAI.SeparableQuotient.Complexify.zero_apply line 24
10. lemma OAI.SeparableQuotient.Complexify.apply_zero line 25
11. lemma OAI.SeparableQuotient.Complexify.apply_add line 26
12. lemma OAI.SeparableQuotient.Complexify.apply_smul line 27
13. def OAI.SeparableQuotient.Complexify.cmul line 29
14. instance OAI.SeparableQuotient.Complexify.(instance at line 30) line 30
15. lemma OAI.SeparableQuotient.Complexify.smul_apply line 31
16. instance OAI.SeparableQuotient.Complexify.(instance at line 34) line 34
17. instance OAI.SeparableQuotient.Complexify.(instance at line 42) line 42
18. instance OAI.SeparableQuotient.Complexify.(instance at line 51) line 51
19. instance OAI.SeparableQuotient.Complexify.(instance at line 57) line 57
20. def OAI.SeparableQuotient.Complexify.pairMap line 63
21. def OAI.SeparableQuotient.Complexify.ofPair line 66
22. lemma OAI.SeparableQuotient.Complexify.pairMap_ofPair line 69
23. lemma OAI.SeparableQuotient.Complexify.ofPair_pairMap line 76
24. def OAI.SeparableQuotient.Complexify.pairEquiv line 83
25. lemma OAI.SeparableQuotient.Complexify.infinite line 89