Metamath Proof Explorer


Table of Contents - 11.1.2. Free modules

According to Wikipedia ("Free module", 03-Mar-2019, https://en.wikipedia.org/wiki/Free_module) "In mathematics, a free module is a module that has a basis - that is, a generating set consisting of linearly independent elements. Every vector space is a free module, but, if the ring of the coefficients is not a division ring (not a field in the commutative case), then there exist non-free modules." The same definition is used in [Lang] p. 135: "By a free module we shall mean a module which admits a basis, or the zero module."

In the following, a free module is defined as the direct sum of copies of a ring regarded as a left module over itself, see df-frlm. Since a module has a basis if and only if it is isomorphic to a free module as defined by df-frlm (see lmisfree), the two definitions are essentially equivalent. The free modules as defined by df-frlm are also taken as a motivation to introduce free modules by [Lang] p. 135.

  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