begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
for
n,
i,
j being
Nat for
K being
Field for
A,
B being
Matrix of
n, st
i in Seg n &
j in Seg n holds
Delete (A + B),
i,
j = (Delete A,i,j) + (Delete B,i,j)
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
Lm1:
for K being Field
for V1, V2 being VectSp of
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
begin
:: deftheorem Def1 defines with_eigenvalues VECTSP11:def 1 :
Lm2:
for K being Field
for V being non trivial VectSp of non trivial holds
( id V is with_eigenvalues & ex v being Vector of st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
:: deftheorem Def2 defines eigenvalue VECTSP11:def 2 :
:: deftheorem Def3 defines eigenvector VECTSP11:def 3 :
theorem
theorem
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem
theorem Th17:
:: deftheorem Def4 defines |^ VECTSP11:def 4 :
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
begin
:: deftheorem Def5 defines UnionKers VECTSP11:def 5 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem
theorem Th36:
theorem Th37:
Lm3:
for K being Field
for V1 being VectSp of
for f being linear-transformation of V1,V1
for a, b being Scalar of holds (a * b) * f = a * (b * f)
Lm4:
for K being Field
for V1 being VectSp of
for L being Scalar of
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
Lm5:
for K being Field
for V1 being VectSp of
for L being Scalar of
for f, g being Function of V1,V1 st f is linear holds
L * (f * g) = f * (L * g)
Lm6:
for K being Field
for V1 being VectSp of
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
Lm7:
for K being Field
for V1 being VectSp of
for f1, f2, g being Function of V1,V1 st g is linear holds
g * (f1 + f2) = (g * f1) + (g * f2)
Lm8:
for K being Field
for V1 being VectSp of
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
Lm9:
for n being Nat
for K being Field
for V1 being VectSp of
for L being Scalar of holds (L * (id V1)) |^ n = ((power K) . L,n) * (id V1)
Lm10:
for K being Field
for V1 being VectSp of
for f being linear-transformation of V1,V1
for a, b being Scalar of holds (a + b) * f = (a * f) + (b * f)
theorem Th38:
theorem
theorem
theorem Th41:
theorem
theorem Th43:
theorem