Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-eigval Structured version   Unicode version

Definition df-eigval 23358
 Description: Define the eigenvalue function. The range of is the set of eigenvalues of Hilbert space operator . Theorem eigvalcl 23465 shows that , the eigenvalue associated with eigenvector , is a complex number. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-eigval
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-eigval
StepHypRef Expression
1 cel 22464 . 2
2 vt . . 3
3 chil 22423 . . . 4
4 cmap 7019 . . . 4
53, 3, 4co 6082 . . 3
6 vx . . . 4
72cv 1652 . . . . 5
8 cei 22463 . . . . 5
97, 8cfv 5455 . . . 4
106cv 1652 . . . . . . 7
1110, 7cfv 5455 . . . . . 6
12 csp 22426 . . . . . 6
1311, 10, 12co 6082 . . . . 5
14 cno 22427 . . . . . . 7
1510, 14cfv 5455 . . . . . 6
16 c2 10050 . . . . . 6
17 cexp 11383 . . . . . 6
1815, 16, 17co 6082 . . . . 5
19 cdiv 9678 . . . . 5
2013, 18, 19co 6082 . . . 4
216, 9, 20cmpt 4267 . . 3
222, 5, 21cmpt 4267 . 2
231, 22wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  eigvalfval  23401
 Copyright terms: Public domain W3C validator