begin
theorem
theorem
theorem Th3:
theorem Th4:
begin
:: deftheorem LMOD_6:def 1 :
canceled;
:: deftheorem Def2 defines trivial LMOD_6:def 2 :
theorem Th5:
theorem
theorem
begin
:: deftheorem defines @ LMOD_6:def 3 :
theorem
canceled;
theorem Th9:
:: deftheorem LMOD_6:def 4 :
canceled;
:: deftheorem defines @ LMOD_6:def 5 :
theorem
theorem
theorem Th12:
theorem Th13:
theorem
canceled;
theorem
begin
:: deftheorem defines <: LMOD_6:def 6 :
begin
:: deftheorem Def7 defines c= LMOD_6:def 7 :
theorem Th16:
theorem
for
K being
Ring for
r being
Scalar of
for
M,
N being
LeftMod of
for
m1,
m2,
m being
Vector of
for
n1,
n2,
n being
Vector of st
M c= N holds
(
0. M = 0. N & (
m1 = n1 &
m2 = n2 implies
m1 + m2 = n1 + n2 ) & (
m = n implies
r * m = r * n ) & (
m = n implies
- n = - m ) & (
m1 = n1 &
m2 = n2 implies
m1 - m2 = n1 - n2 ) &
0. N in M &
0. M in N & (
n1 in M &
n2 in M implies
n1 + n2 in M ) & (
n in M implies
r * n in M ) & (
n in M implies
- n in M ) & (
n1 in M &
n2 in M implies
n1 - n2 in M ) )
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem