mathlib3

65e3b049 - feat(linear_algebra/determinant): various `basis.det` lemmas (#7669)

feat(linear_algebra/determinant): various `basis.det` lemmas (#7669) A selection of results that I needed for computing the value of `basis.det`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>