mathlib3

9f1b9bcd - feat(linear_algebra/determinant): more properties of the determinant of linear maps (#10809)