mathlib3

b9fcf9b1 - feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib (#8682)

feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib (#8682) We prove that the adjugate of a matrix distributes over the product. To do so, a separate file `linear_algebra.matrix.polynomial` states some general facts about the polynomial `det (t I + A)`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>