Metamath Proof Explorer


Table of Contents - 20.43.21.3. Linear independence

According to the definition in [Lang] p. 129: "A subset S of a module M is said to be <b>linearly independent</b> (over [the ring] A) if whenever we have a linear combination &sum;<sub>x &isin;S</sub> a<sub>x</sub>x which is equal to 0, then a<sub>x</sub>=0 for all x&isin;S." This definition does not care for the finiteness of the set S (because the definition of a linear combination in [Lang] p.129 does already assure that only a finite number of coefficients can be 0 in the sum). Our definition df-lininds does also neither claim that the subset must be finite, nor that almost all coefficients within the linear combination are 0. If this is required, it must be explicitly stated as precondition in the corresponding theorems.<br> <br> Usually, the linear independence is defined for vector spaces, see Wikipedia ("Linear independence", 15-Apr-2019, https://en.wikipedia.org/wiki/Linear_independence): "In the theory of vector spaces, a set of vectors is said to be <b>linearly dependent</b> if at least one of the vectors in the set can be defined as a linear combination of the others; if no vector in the set can be written in this way, then the vectors are said to be <b>linearly independent</b>." Furthermore, "In order to allow the number of linearly independent vectors in a vector space to be countably infinite, it is useful to define linear dependence as follows. More generally, let V be a vector space over a field K, and let {v<sub>i</sub> | i&isin;I} be a family of elements of V. The family is linearly dependent over K if there exists a finite family {a<sub>j</sub> | j&isin;J} of elements of K, all nonzero, such that &sum;<sub>j&isin;J</sub> a<sub>j</sub>v<sub>j</sub>=0. A set X of elements of V is linearly independent if the corresponding family{x}<sub>x&isin;X</sub> is linearly independent". <br> <b>Remark 1:</b> There are already definitions of (linearly) independent families (df-lindf) and (linearly) independent sets (df-linds). These definitions are based on the principle "of vectors, no nonzero multiple of which can be expressed as a linear combination of other elements" or (see lbsind2) "every element is not in the span of the remainder of the [set]". The equivalence of the definitions df-linds and df-lininds for (linear) independence for (left) modules is shown in lindslininds. <br> <b>Remark 2:</b> Subsets of the base set of a (left) module are <b>linearly dependent</b> if they are not linearly independent (see df-lindeps) or, according to Wikipedia, "if at least one of the vectors in the set can be defined as a linear combination of the others", see islindeps2. The reversed implication is not valid for arbitrary modules (but for arbitrary vector spaces), because it requires a division by a coefficient. Therefore, the definition of Wikipedia is equivalent to our definition for (left) vector spaces (see isldepslvec2) and not for (left) modules in general.

  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