mathlib3 documentation

linear_algebra.matrix.charpoly.minpoly

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) :
@[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) :
theorem matrix.is_integral {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : matrix n n R) :
theorem matrix.minpoly_dvd_charpoly {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] (M : matrix n n K) :
@[simp]
theorem linear_map.minpoly_to_matrix' {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (f : (n R) →ₗ[R] n R) :
@[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) :
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.