mathlib3

bf2301b4 - feat(linear_algebra/matrix): some bounds on the determinant of matrices

feat(linear_algebra/matrix): some bounds on the determinant of matrices This PR shows that matrices with bounded entries also have bounded determinants. `matrix.det_le` is the most generic version of these results, which we specialise to `matrix.det_sum_smul_le`. In a follow-up PR we connect this to `algebra.left_mul_matrix` to provide an upper bound on `algebra.norm`.