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 matrix
det_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.
The characteristic polynomial of the map
λ x, a * x is the minimal polynomial of
In combination with
and a bit of rewriting, this will allow us to conclude the
field norm resp. trace of
x is the product resp. sum of