Metamath Proof Explorer

Table of Contents - 20.43.21. Linear algebra (extension)

1. The subalgebras of diagonal and scalar matrices (extension)
   1. cdmatalt
   2. cscmatalt
   3. df-dmatalt
   4. df-scmatalt
   5. dmatALTval
   6. dmatALTbas
   7. dmatALTbasel
   8. dmatbas
2. Linear combinations
   1. clinc
   2. clinco
   3. df-linc
   4. df-lco
   5. lincop
   6. lincval
   7. dflinc2
   8. lcoop
   9. lcoval
   10. lincfsuppcl
   11. linccl
   12. lincval0
   13. lincvalsng
   14. lincvalsn
   15. lincvalpr
   16. lincval1
   17. lcosn0
   18. lincvalsc0
   19. lcoc0
   20. linc0scn0
   21. lincdifsn
   22. linc1
   23. lincellss
   24. lco0
   25. lcoel0
   26. lincsum
   27. lincscm
   28. lincsumcl
   29. lincscmcl
   30. lincsumscmcl
   31. lincolss
   32. ellcoellss
   33. lcoss
   34. lspsslco
   35. lcosslsp
   36. lspeqlco
3. Linear independence
   1. clininds
   2. clindeps
   3. df-lininds
   4. rellininds
   5. df-lindeps
   6. linindsv
   7. islininds
   8. linindsi
   9. linindslinci
   10. islinindfis
   11. islinindfiss
   12. linindscl
   13. lindepsnlininds
   14. islindeps
   15. lincext1
   16. lincext2
   17. lincext3
   18. lindslinindsimp1
   19. lindslinindimp2lem1
   20. lindslinindimp2lem2
   21. lindslinindimp2lem3
   22. lindslinindimp2lem4
   23. lindslinindsimp2lem5
   24. lindslinindsimp2
   25. lindslininds
   26. linds0
   27. el0ldep
   28. el0ldepsnzr
   29. lindsrng01
   30. lindszr
   31. snlindsntorlem
   32. snlindsntor
   33. ldepsprlem
   34. ldepspr
   35. lincresunit3lem3
   36. lincresunitlem1
   37. lincresunitlem2
   38. lincresunit1
   39. lincresunit2
   40. lincresunit3lem1
   41. lincresunit3lem2
   42. lincresunit3
   43. lincreslvec3
   44. islindeps2
   45. islininds2
   46. isldepslvec2
   47. lindssnlvec
4. Simple left modules and the ` ZZ `-module
   1. lmod1lem1
   2. lmod1lem2
   3. lmod1lem3
   4. lmod1lem4
   5. lmod1lem5
   6. lmod1
   7. lmod1zr
   8. lmod1zrnlvec
   9. lmodn0
   10. zlmodzxzequa
   11. zlmodzxznm
   12. zlmodzxzldeplem
   13. zlmodzxzequap
   14. zlmodzxzldeplem1
   15. zlmodzxzldeplem2
   16. zlmodzxzldeplem3
   17. zlmodzxzldeplem4
   18. zlmodzxzldep
   19. ldepsnlinclem1
   20. ldepsnlinclem2
5. Differences between (left) modules and (left) vector spaces
   1. lvecpsslmod
   2. ldepsnlinc
   3. ldepslinc