begin
Lm1:
for R being Ring
for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
theorem Th1:
Lm2:
for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
theorem
theorem
theorem
:: deftheorem RMOD_4:def 1 :
canceled;
:: deftheorem RMOD_4:def 2 :
canceled;
:: deftheorem Def3 defines Sum RMOD_4:def 3 :
theorem Th5:
theorem
theorem
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
theorem
:: deftheorem Def4 defines Linear_Combination RMOD_4:def 4 :
:: deftheorem defines Carrier RMOD_4:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem Def6 defines ZeroLC RMOD_4:def 6 :
theorem
canceled;
theorem Th22:
:: deftheorem Def7 defines Linear_Combination RMOD_4:def 7 :
theorem
canceled;
theorem
canceled;
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem Def8 defines (#) RMOD_4:def 8 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem
theorem Th37:
:: deftheorem Def9 defines Sum RMOD_4:def 9 :
Lm3:
for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V
theorem
canceled;
theorem
canceled;
theorem Th40:
theorem
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem
:: deftheorem defines = RMOD_4:def 10 :
:: deftheorem Def11 defines + RMOD_4:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem
:: deftheorem Def12 defines * RMOD_4:def 12 :
theorem
canceled;
theorem
canceled;
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem
theorem Th64:
theorem
:: deftheorem defines - RMOD_4:def 13 :
theorem
canceled;
theorem Th67:
theorem
theorem Th69:
theorem
:: deftheorem defines - RMOD_4:def 14 :
theorem
canceled;
theorem
canceled;
theorem Th73:
theorem
theorem
theorem
theorem Th77:
theorem Th78:
theorem Th79:
theorem
begin
:: deftheorem Def15 defines linearly-independent RMOD_4:def 15 :
theorem
theorem Th82:
theorem
theorem Th84:
theorem
:: deftheorem Def16 defines Lin RMOD_4:def 16 :
theorem Th86:
theorem Th87:
theorem
theorem
theorem Th90:
theorem
theorem Th92:
theorem
theorem
theorem