:: deftheorem defines linearly-independent RMOD_4:def 13 :
for R being Ring
for V being RightMod of R
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );