Characteristic polynomial #
We define the characteristic polynomial of f : M →ₗ[R] M
, where M
is a finite and
free R
-module. The proof that f.charpoly
is the characteristic polynomial of the matrix of f
in any basis is in linear_algebra/charpoly/to_matrix
.
Main definition #
linear_map.charpoly f
: the characteristic polynomial off : M →ₗ[R] M
.
noncomputable
def
linear_map.charpoly
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
(f : M →ₗ[R] M) :
R[X]
The characteristic polynomial of f : M →ₗ[R] M
.
Equations
- f.charpoly = (⇑(linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R M)) f).charpoly
theorem
linear_map.charpoly_def
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
(f : M →ₗ[R] M) :
f.charpoly = (⇑(linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R M)) f).charpoly
theorem
linear_map.charpoly_monic
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
(f : M →ₗ[R] M) :
theorem
linear_map.aeval_self_charpoly
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
(f : M →ₗ[R] M) :
⇑(polynomial.aeval f) f.charpoly = 0
The Cayley-Hamilton Theorem, that the characteristic polynomial of a linear map, applied to the linear map itself, is zero.
theorem
linear_map.is_integral
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
(f : M →ₗ[R] M) :
is_integral R f
theorem
linear_map.minpoly_dvd_charpoly
{K : Type u}
{M : Type v}
[field K]
[add_comm_group M]
[module K M]
[finite_dimensional K M]
(f : M →ₗ[K] M) :
theorem
linear_map.minpoly_coeff_zero_of_injective
{R : Type u}
{M : Type v}
[comm_ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
{f : M →ₗ[R] M}
(hf : function.injective ⇑f) :