Characteristic polynomials #
We give methods for computing coefficients of the characteristic polynomial.
Main definitions #
matrix.charpoly_degree_eq_dimproves that the degree of the characteristic polynomial over a nonzero ring is the dimension of the matrix
matrix.det_eq_sign_charpoly_coeffproves that the determinant is the constant term of the characteristic polynomial, up to sign.
matrix.trace_eq_neg_charpoly_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