mathlib3

974d413b - chore(linear_algebra/determinant): simplify det_mul proof (#1392)

chore(linear_algebra/determinant): simplify det_mul proof (#1392) * chore(linear_algebra/determinant): simplify det_mul proof Minor improvement to the proof of `det_mul` * make det_mul_aux more readable