# mathlibdocumentation

linear_algebra.matrix.charpoly.coeff

# Characteristic polynomials #

We give methods for computing coefficients of the characteristic polynomial.

## Main definitions #

• matrix.charpoly_degree_eq_dim proves that the degree of the characteristic polynomial over a nonzero ring is the dimension of the matrix
• matrix.det_eq_sign_charpoly_coeff proves that the determinant is the constant term of the characteristic polynomial, up to sign.
• matrix.trace_eq_neg_charpoly_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 charmatrix_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 charmatrix_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 matrix.charpoly_sub_diagonal_degree_lt {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
theorem matrix.charpoly_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) :
theorem matrix.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 matrix.charpoly_degree_eq_dim {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] [nontrivial R] (M : n R) :
theorem matrix.charpoly_nat_degree_eq_dim {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] [nontrivial R] (M : n R) :
theorem matrix.charpoly_monic {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
theorem matrix.trace_eq_neg_charpoly_coeff {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] [nonempty n] (M : n R) :
theorem matrix.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 matrix.eval_det {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n (polynomial R)) (r : R) :
theorem matrix.det_eq_sign_charpoly_coeff {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) :
M.det = (-1) ^ * M.charpoly.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) :
theorem matrix.aeval_eq_aeval_mod_charpoly {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) (p : polynomial R) :
p = (p %ₘ M.charpoly)

Any matrix polynomial p is equivalent under evaluation to p %ₘ M.charpoly; that is, p is equivalent to a polynomial with degree less than the dimension of the matrix.

theorem matrix.pow_eq_aeval_mod_charpoly {R : Type u} [comm_ring R] {n : Type v} [decidable_eq n] [fintype n] (M : n R) (k : ) :
M ^ k = %ₘ M.charpoly)

Any matrix power can be computed as the sum of matrix powers less than fintype.card n.

TODO: add the statement for negative powers phrased with zpow.