Solutions_S03_Endomorphisms.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

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) line 35 source
example (example at line 48) line 48 source