mathlib

9abfa6f0 - refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565)

refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565) A handful of these results can be proven trivially using results about `is_self_adjoint`. This also generalizes the typeclass arguments throughout the file, though largely in a mathematically meaningless way.