# mathlibdocumentation

linear_algebra.char_poly.coeff

# Characteristic polynomials #

We give methods for computing coefficients of the characteristic polynomial.

## Main definitions #

• char_poly_degree_eq_dim proves that the degree of the characteristic polynomial over a nonzero ring is the dimension of the matrix
• det_eq_sign_char_poly_coeff proves that the determinant is the constant term of the characteristic polynomial, up to sign.
• trace_eq_neg_char_poly_coeff proves that the trace is the negative of the (d-1)th coefficient of the characteristic polynomial, where d is the dimension of the matrix. For a nonzero ring, this is the second-highest coefficient.
theorem char_matrix_apply_nat_degree {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] {M : n R} [nontrivial R] (i j : n) :
i j).nat_degree = ite (i = j) 1 0
theorem char_matrix_apply_nat_degree_le {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] {M : n R} (i j : n) :
i j).nat_degree ite (i = j) 1 0
theorem char_poly_sub_diagonal_degree_lt {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
- ∏ (i : n), (polynomial.X - polynomial.C (M i i))).degree < - 1)
theorem char_poly_coeff_eq_prod_coeff_of_le {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) {k : } (h : k) :
(char_poly M).coeff k = (∏ (i : n), (polynomial.X - polynomial.C (M i i))).coeff k
theorem det_of_card_zero {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (h : = 0) (M : n R) :
M.det = 1
theorem char_poly_degree_eq_dim {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] [nontrivial R] (M : n R) :
theorem char_poly_nat_degree_eq_dim {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] [nontrivial R] (M : n R) :
theorem char_poly_monic {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
theorem trace_eq_neg_char_poly_coeff {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] [nonempty n] (M : n R) :
R R) M = -(char_poly M).coeff - 1)
theorem mat_poly_equiv_eval {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n (polynomial R)) (r : R) (i j : n) :
polynomial.eval ( r) i j = (M i j)
theorem eval_det {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n (polynomial R)) (r : R) :
theorem det_eq_sign_char_poly_coeff {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
M.det = ((-1) ^ * (char_poly M).coeff 0
theorem mat_poly_equiv_eq_X_pow_sub_C {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} (k : ) [field K] (M : n K) :
@[simp]
theorem finite_field.char_poly_pow_card {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] [fintype K] (M : n K) :
@[simp]
theorem zmod.char_poly_pow_card {n : Type v} [decidable_eq n] [fintype n] {p : } [fact (nat.prime p)] (M : n (zmod p)) :
char_poly (M ^ p) =
theorem finite_field.trace_pow_card {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] [fintype K] [nonempty n] (M : n K) :
K K) (M ^ = K K) M ^
theorem zmod.trace_pow_card {n : Type v} [decidable_eq n] [fintype n] {p : } [fact (nat.prime p)] [nonempty n] (M : n (zmod p)) :
(zmod p) (zmod p)) (M ^ p) = (zmod p) (zmod p)) M ^ p
theorem matrix.is_integral {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
M
theorem matrix.min_poly_dvd_char_poly {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] (M : n K) :
M
theorem char_poly_left_mul_matrix {K : Type u_1} {S : Type u_2} [field K] [comm_ring S] [ S] (h : S) :
= h.gen

The characteristic polynomial of the map λ x, a * x is the minimal polynomial of a.

In combination with det_eq_sign_char_poly_coeff or trace_eq_neg_char_poly_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.