mathlib

ce62dbc3 - feat(algebra/star/self_adjoint): module instance on self-adjoint elements of a star algebra (#11322)

feat(algebra/star/self_adjoint): module instance on self-adjoint elements of a star algebra (#11322) We put a module instance on `self_adjoint A`, where `A` is a `[star_module R A]` and `R` has a trivial star operation. A new typeclass `[has_trivial_star R]` is created for this purpose with an instance on `ℝ`. This allows us to express the fact that e.g. the space of complex Hermitian matrices is a real vector space.