mathlib3

f46fcef9 - feat(matrix/spectrum): The determinant of a hermitian matrix is the product of its eigenvalues. (#16293)