begin
Lm1:
for R being Ring
for a being Scalar of st - a = 0. R holds
a = 0. R
theorem
canceled;
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th6:
theorem Th7:
:: deftheorem Def1 defines Lin MOD_3:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
theorem Th17:
theorem
theorem
theorem
:: deftheorem Def2 defines base MOD_3:def 2 :
:: deftheorem Def3 defines free MOD_3:def 3 :
theorem Th21:
Lm2:
for R being Skew-Field
for a being Scalar of
for V being LeftMod of
for v being Vector of st a <> 0. R holds
( (a " ) * (a * v) = (1. R) * v & ((a " ) * a) * v = (1. R) * v )
theorem
canceled;
theorem
theorem Th24:
theorem
theorem Th26:
theorem Th27:
Lm3:
for R being Skew-Field
for V being LeftMod of ex B being Subset of st B is base
theorem
:: deftheorem MOD_3:def 4 :
canceled;
:: deftheorem Def5 defines Basis MOD_3:def 5 :
theorem
theorem