S03_Endomorphisms.lean`

12 declarations, 2 contain sorry, 0 declared as axioms

Imports (4)

Imported by 1 file

example (example at line 18) line 18 source
example (example at line 22) line 22 source
Source comment
evaluating `P` on `φ`
```
example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
…
```
example (example at line 26) line 26 source
Source comment
evaluating `X` on `φ` gives back `φ`
```
example (φ : End K V) : aeval φ (X : K[X]) = φ :=
…
```
example (example at line 35) sorry line 35 source
example (example at line 43) sorry line 43 source
example (example at line 46) line 46 source
example (example at line 51) line 51 source
example (example at line 54) line 54 source
example (example at line 57) line 57 source
example (example at line 61) line 61 source
Source comment
Eigenvalue are roots of the minimal polynomial
```
example (φ : End K V) (a : K) : φ.HasEigenvalue a → (minpoly K φ).IsRoot a :=
…
```
example (example at line 65) line 65 source
Source comment
In finite dimension, the converse is also true (we will discuss dimension below)
```
example [FiniteDimensional K V] (φ : End K V) (a : K) :
    φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
…
```

example (example at line 70) line 70 source

Source comment

Cayley-Hamilton

example [FiniteDimensional K V] (φ : End K V) : aeval φ φ.charpoly = 0 :=
…