Commit 2021-08-27 10:03 88e47d7c
View on Github →feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib_aux (#8681) We prove towards the fact that the adjugate of a matrix distributes over the product. The current proof assumes regularity of the matrices. In the general case, this hypothesis is not required, but this lemma will be crucial in a follow-up PR which has to use polynomial matrices for the general case. Additionally, we provide many API lemmas for det, cramer, nonsing_inv, and adjugate.