Commit 2021-08-20 14:42 d62a4614

feat(linear_algebra/determinant): det (M ⬝ N) = det (N ⬝ M) if M is invertible (#8720) If M is a square or invertible matrix, then det (M ⬝ N) = det (N ⬝ M). This is basically just using mul_comm on det M * det N, except for some tricky rewriting to handle the invertible case.