:: Eigenvalues of a Linear Transformation
:: by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: VECTSP11:1
theorem Th2: :: VECTSP11:2
theorem Th3: :: VECTSP11:3
theorem Th4: :: VECTSP11:4
for
n,
i,
j being
Nat for
K being
Field for
A,
B being
Matrix of
n,
K 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: :: VECTSP11:5
theorem Th6: :: VECTSP11:6
theorem Th7: :: VECTSP11:7
theorem Th8: :: VECTSP11:8
Lm1:
for K being Field
for V1, V2 being VectSp of K
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
:: deftheorem Def1 defines with_eigenvalues VECTSP11:def 1 :
Lm2:
for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues & ex v being Vector of V 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 :: VECTSP11:9
theorem :: VECTSP11:10
theorem Th11: :: VECTSP11:11
theorem :: VECTSP11:12
theorem :: VECTSP11:13
theorem Th14: :: VECTSP11:14
theorem Th15: :: VECTSP11:15
theorem :: VECTSP11:16
theorem Th17: :: VECTSP11:17
:: deftheorem Def4 defines |^ VECTSP11:def 4 :
theorem Th18: :: VECTSP11:18
theorem Th19: :: VECTSP11:19
theorem Th20: :: VECTSP11:20
theorem :: VECTSP11:21
theorem :: VECTSP11:22
theorem Th23: :: VECTSP11:23
:: deftheorem Def5 defines UnionKers VECTSP11:def 5 :
theorem Th24: :: VECTSP11:24
theorem Th25: :: VECTSP11:25
theorem Th26: :: VECTSP11:26
theorem :: VECTSP11:27
theorem Th28: :: VECTSP11:28
theorem :: VECTSP11:29
theorem Th30: :: VECTSP11:30
theorem Th31: :: VECTSP11:31
theorem Th32: :: VECTSP11:32
theorem :: VECTSP11:33
theorem Th34: :: VECTSP11:34
theorem :: VECTSP11:35
theorem Th36: :: VECTSP11:36
theorem Th37: :: VECTSP11:37
Lm3:
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
Lm4:
for K being Field
for V1 being VectSp of K
for L being Scalar of K
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 K
for L being Scalar of K
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 K
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 K
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 K
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 K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . L,n) * (id V1)
Lm10:
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)
theorem Th38: :: VECTSP11:38
theorem :: VECTSP11:39
theorem :: VECTSP11:40
theorem Th41: :: VECTSP11:41
theorem :: VECTSP11:42
theorem Th43: :: VECTSP11:43
theorem :: VECTSP11:44