mathlib

ab0a2959 - feat(linear_algebra/matrix): some bounds on the determinant of matrices (#9029)

feat(linear_algebra/matrix): some bounds on the determinant of matrices (#9029) 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 in two steps to `matrix.det_sum_smul_le`. In a follow-up PR we will connect this to `algebra.left_mul_matrix` to provide an upper bound on `algebra.norm`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>