mathlib

282e3613 - feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib_aux

feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib_aux 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.