Metamath Proof Explorer

Table of Contents - 11.1. Vectors and free modules

Direct sum of left modules
1. cdsmm
2. df-dsmm
3. reldmdsmm
4. dsmmval
5. dsmmbase
6. dsmmval2
7. dsmmbas2
8. dsmmfi
9. dsmmelbas
10. dsmm0cl
11. dsmmacl
12. prdsinvgd2
13. dsmmsubg
14. dsmmlss
15. dsmmlmod
Free modules
1. cfrlm
2. df-frlm
3. frlmval
4. frlmlmod
5. frlmpws
6. frlmlss
7. frlmpwsfi
8. frlmsca
9. frlm0
10. frlmbas
11. frlmelbas
12. frlmrcl
13. frlmbasfsupp
14. frlmbasmap
15. frlmbasf
16. frlmlvec
17. frlmfibas
18. elfrlmbasn0
19. frlmplusgval
20. frlmsubgval
21. frlmvscafval
22. frlmvplusgvalc
23. frlmvscaval
24. frlmplusgvalb
25. frlmvscavalb
26. frlmvplusgscavalb
27. frlmgsum
28. frlmsplit2
29. frlmsslss
30. frlmsslss2
31. frlmbas3
32. mpofrlmd
33. frlmip
34. frlmipval
35. frlmphllem
36. frlmphl
Standard basis (unit vectors)
1. cuvc
2. df-uvc
3. uvcfval
4. uvcval
5. uvcvval
6. uvcvvcl
7. uvcvvcl2
8. uvcvv1
9. uvcvv0
10. uvcff
11. uvcf1
12. uvcresum
13. frlmssuvc1
14. frlmssuvc2
15. frlmsslsp
16. frlmlbs
17. frlmup1
18. frlmup2
19. frlmup3
20. frlmup4
21. ellspd
22. elfilspd
Independent sets and families
1. clindf
2. clinds
3. df-lindf
4. df-linds
5. rellindf
6. islinds
7. linds1
8. linds2
9. islindf
10. islinds2
11. islindf2
12. lindff
13. lindfind
14. lindsind
15. lindfind2
16. lindsind2
17. lindff1
18. lindfrn
19. f1lindf
20. lindfres
21. lindsss
22. f1linds
23. islindf3
24. lindfmm
25. lindsmm
26. lindsmm2
27. lsslindf
28. lsslinds
29. islbs4
30. lbslinds
31. islinds3
32. islinds4
Characterization of free modules
1. lmimlbs
2. lmiclbs
3. islindf4
4. islindf5
5. indlcim
6. lbslcic
7. lmisfree
8. lvecisfrlm
9. lmimco
10. lmictra
11. uvcf1o
12. uvcendim
13. frlmisfrlm
14. frlmiscvec