Commit 2023-08-21 17:56 590f2c48

View on Github →

feat: characterise the reverse of the characteristic polynomial of a matrix (#6561)

Estimated changes

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

modified theorem Polynomial.degree_X_pow

added theorem Polynomial.natDegree_X_mul

modified theorem Polynomial.natDegree_X_pow

added theorem Polynomial.natDegree_X_pow_mul

added theorem Polynomial.natDegree_mul_X

added theorem Polynomial.natDegree_mul_X_pow

Modified Mathlib/Data/Polynomial/Laurent.lean

added theorem LaurentPolynomial.C_apply

added theorem LaurentPolynomial.T_apply

added def LaurentPolynomial.invert

added theorem LaurentPolynomial.invert_C

added theorem LaurentPolynomial.invert_T

added theorem LaurentPolynomial.invert_apply

added theorem LaurentPolynomial.invert_comp_C

added theorem LaurentPolynomial.invert_symm

added theorem LaurentPolynomial.involutive_invert

added theorem LaurentPolynomial.toLaurent_reverse

added theorem Polynomial.coe_toLaurentAlg

added theorem Polynomial.toLaurent_comp_C

Modified Mathlib/Data/Polynomial/Reverse.lean

added theorem Polynomial.reflect_one_X

added theorem Polynomial.reverse_C

added theorem Polynomial.reverse_C_add

added theorem Polynomial.reverse_X_mul

added theorem Polynomial.reverse_X_pow_mul

added theorem Polynomial.reverse_add_C

added theorem Polynomial.reverse_mul_X

added theorem Polynomial.reverse_mul_X_pow

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

added theorem Matrix.reverse_charpoly