Characteristic polynomials
We give methods for computing coefficients of the characteristic polynomial.
Main definitions
char_poly_degree_eq_dimproves that the degree of the characteristic polynomial over a nonzero ring is the dimension of the matrixdet_eq_sign_char_poly_coeffproves that the determinant is the constant term of the characteristic polynomial, up to sign.trace_eq_neg_char_poly_coeffproves 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 : matrix n n R}
[nontrivial R]
(i j : n) :
(char_matrix M 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 : matrix n n R}
(i j : n) :
(char_matrix M 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 : matrix n n R) :
(char_poly M - finset.univ.prod (λ (i : n), polynomial.X - ⇑polynomial.C (M i i))).degree < ↑(fintype.card n - 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 : matrix n n R)
{k : ℕ} :
fintype.card n - 1 ≤ k → (char_poly M).coeff k = (finset.univ.prod (λ (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 : fintype.card n = 0)
(M : matrix n n R) :
theorem
char_poly_degree_eq_dim
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
[nontrivial R]
(M : matrix n n R) :
(char_poly M).degree = ↑(fintype.card n)
theorem
char_poly_nat_degree_eq_dim
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
[nontrivial R]
(M : matrix n n R) :
(char_poly M).nat_degree = fintype.card n
theorem
char_poly_monic_of_nontrivial
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
[nontrivial R]
(M : matrix n n R) :
theorem
char_poly_monic
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n 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 : matrix n n R) :
⇑(matrix.trace n R R) M = -(char_poly M).coeff (fintype.card n - 1)
theorem
mat_poly_equiv_eval
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n (polynomial R))
(r : R)
(i j : n) :
polynomial.eval (⇑(matrix.scalar n) r) (⇑mat_poly_equiv M) i j = polynomial.eval r (M i j)
theorem
eval_det
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n (polynomial R))
(r : R) :
polynomial.eval r M.det = (polynomial.eval (⇑(matrix.scalar n) r) (⇑mat_poly_equiv M)).det
theorem
det_eq_sign_char_poly_coeff
{R : Type u}
[comm_ring R]
{n : Type v}
[decidable_eq n]
[fintype n]
(M : matrix n n R) :