Commit 2021-09-09 16:13 b9fcf9b1

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