mathlib documentation

linear_algebra.char_poly.coeff

Characteristic polynomials

We give methods for computing coefficients of the characteristic polynomial.

Main definitions

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 - ∏ (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 = (∏ (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) :
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 : matrix n 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 : 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) :

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) :

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) :

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) :
M.det = ((-1) ^ fintype.card n) * (char_poly M).coeff 0

@[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 : matrix n n K) :

@[simp]
theorem zmod.char_poly_pow_card {n : Type v} [decidable_eq n] [fintype n] {p : } [fact (nat.prime p)] (M : matrix n n (zmod 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 : matrix n n K) :

theorem zmod.trace_pow_card {n : Type v} [decidable_eq n] [fintype n] {p : } [fact (nat.prime p)] [nonempty n] (M : matrix n n (zmod p)) :
(matrix.trace n (zmod p) (zmod p)) (M ^ p) = (matrix.trace n (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 : matrix n n R) :

theorem matrix.min_poly_dvd_char_poly {n : Type v} [decidable_eq n] [fintype n] {K : Type u_1} [field K] (M : matrix n n K) :