The minimal polynomial divides the characteristic polynomial of a matrix. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This also includes some miscellaneous results about minpoly on matrices.
@[simp]
theorem
matrix.minpoly_to_lin'
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
minpoly R (⇑matrix.to_lin' M) = minpoly R M
@[simp]
theorem
matrix.minpoly_to_lin
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
{N : Type w}
[add_comm_group N]
[module R N]
(b : basis n R N)
(M : matrix n n R) :
minpoly R (⇑(matrix.to_lin b b) M) = minpoly R M
theorem
matrix.is_integral
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :
is_integral R M
@[simp]
theorem
linear_map.minpoly_to_matrix
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
{N : Type w}
[add_comm_group N]
[module R N]
(b : basis n R N)
(f : N →ₗ[R] N) :
minpoly R (⇑(linear_map.to_matrix b b) f) = minpoly R f
theorem
charpoly_left_mul_matrix
{R : Type u}
[comm_ring R]
{S : Type u_1}
[ring S]
[algebra R S]
(h : power_basis R S) :
The characteristic polynomial of the map λ x, a * x is the minimal polynomial of a.
In combination with det_eq_sign_charpoly_coeff or trace_eq_neg_charpoly_coeff
and a bit of rewriting, this will allow us to conclude the
field norm resp. trace of x is the product resp. sum of x's conjugates.