Description: The reverse implication of islindeps2 does not hold for arbitrary (left) modules, see note in Roman p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa and zlmodzxznm . (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ldepsnlinc | |